From cbe7dd4a48780db2268ec52a60b880af3a21ea48 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Sep 2021 14:26:09 -0700
Subject: [PATCH] missing continue fixes unsound sat result from #5573
---
src/sat/smt/euf_solver.cpp | 2 ++
src/sat/smt/q_ematch.cpp | 4 +++-
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 753ec37da..3c3b6e884 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -490,6 +490,8 @@ namespace euf {
apply_solver(m_qsolver);
if (num_nodes < m_egraph.num_nodes())
return sat::check_result::CR_CONTINUE;
+ if (cont)
+ return sat::check_result::CR_CONTINUE;
TRACE("after_search", s().display(tout););
if (give_up)
return sat::check_result::CR_GIVEUP;
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index cb5144a2b..2d8ac8afd 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -605,7 +605,9 @@ namespace q {
}
if (propagate(true))
return true;
- return m_inst_queue.lazy_propagate();
+ if (m_inst_queue.lazy_propagate())
+ return true;
+ return false;
}
void ematch::collect_statistics(statistics& st) const {