From 78c7749478ba9152065349f888ae15a5732c409d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 27 Jul 2018 10:19:13 -0500
Subject: [PATCH]  Make check-synth robust for assertions that are not the
 synth conjecture (#2217)

---
 src/smt/smt_engine.cpp | 5 +++++
 1 file changed, 5 insertions(+)

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;
-- 
2.30.2