From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 27 Jul 2018 15:19:13 +0000 (-0500)
Subject:  Make check-synth robust for assertions that are not the synth conjecture (#2217)
X-Git-Tag: cvc5-1.0.0~4852
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78c7749478ba9152065349f888ae15a5732c409d;p=cvc5.git

 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 d807567b7..5296a3bca 100644
--- 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;