Make check-synth robust for assertions that are not the synth conjecture (#2217)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d807567b70f349c20cba76ba4b39503d52ce491c..5296a3bca0a088de7bd14f6092f43cbe2313bef8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5581,6 +5581,11 @@ void SmtEngine::checkSynthSolution()
     }
     Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << conj << endl;
     Trace("check-synth-sol") << "Expanded assertion " << conj << "\n";
+    if (conj.getKind() != kind::FORALL)
+    {
+      Trace("check-synth-sol") << "Not a checkable assertion.\n";
+      continue;
+    }
 
     // Apply solution map to conjecture body
     Node conjBody;