diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index f646ff014..5aa9d2c13 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -608,12 +608,21 @@ bool CompilerStack::analyze()
 			if (m_modelCheckerSettings.engine.any())
 				m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter);
 
-			ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile);
-			modelChecker.checkRequestedSourcesAndContracts(allSources);
-			for (Source const* source: m_sourceOrder)
-				if (source->ast)
-					modelChecker.analyze(*source->ast);
-			m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();
+			if (m_modelCheckerSettings.engine.any() && !m_readFile)
+				m_errorReporter.warning(
+						7126_error,
+						SourceLocation(),
+						"Model checker analysis requested but no callback for SMT queries was provided, ignoring!"
+				);
+			else
+			{
+				ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile);
+				modelChecker.checkRequestedSourcesAndContracts(allSources);
+				for (Source const* source: m_sourceOrder)
+					if (source->ast)
+						modelChecker.analyze(*source->ast);
+				m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();
+			}
 		}
 	}
 	catch (FatalError const&)
diff --git a/scripts/error_codes.py b/scripts/error_codes.py
index 33a475214..34e44547e 100755
--- a/scripts/error_codes.py
+++ b/scripts/error_codes.py
@@ -207,6 +207,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
         "2961", # SMTChecker, covered by CL tests
         "6240", # SMTChecker, covered by CL tests
         "9576", # SMTChecker, covered by CL tests
+        "7126", # SMTChecker, analysis without callback (not sure how to cover this)
     }
     assert len(test_ids & white_ids) == 0, "The sets are not supposed to intersect"
     test_ids |= white_ids