From fcd1f2b3cd4ed6dae913f418f8b95235402ff5e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 21 Mar 2020 17:45:54 -0700 Subject: [PATCH] fix #3459 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- src/tactic/sine_filter.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ed44eb642..8600a3d3a 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4459,8 +4459,8 @@ namespace smt { if (has_case_splits()) return false; fcs = final_check(); + TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";); } - TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";); if (fcs == FC_DONE) { reset_model(); } diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index cca8a906c..781150a6a 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -215,6 +215,8 @@ private: visiting = to_visit.back(); to_visit.pop_back(); visited.insert(visiting); + if (!exp2const.contains(visiting)) + continue; for (func_decl* f : exp2const[visiting]) for (expr* e : const2exp[f]) { if (!visited.contains(e))