From fadc3761bd3924b1c9164f1844b0767151bf123c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Apr 2020 17:06:43 -0700 Subject: [PATCH] fix #3731 - abuse of parameter combinations, trying to use qsat on arrays, but disabling array equality expansion during model evaluation Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arith.cpp | 2 +- src/qe/qsat.cpp | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 70a0e6a99..c30e77cc9 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -65,7 +65,7 @@ namespace qe { DEBUG_CODE(expr_ref val(m); eval(lit, val); CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";); - SASSERT(m.limit().get_cancel_flag() || m.is_true(val));); + SASSERT(m.limit().get_cancel_flag() || !m.is_false(val));); if (!m.inc()) return false; diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index aa1cc2eb3..cdf89fa9f 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -29,6 +29,7 @@ Notes: #include "ast/rewriter/expr_replacer.h" #include "model/model_v2_pp.h" #include "model/model_evaluator.h" +#include "model/model_evaluator_params.hpp" #include "smt/smt_kernel.h" #include "smt/params/smt_params.h" #include "smt/smt_solver.h" @@ -1254,6 +1255,9 @@ namespace qe { void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result) override { tactic_report report("qsat-tactic", *in); + model_evaluator_params mp(m_params); + if (!mp.array_equalities()) + throw tactic_exception("array equalities cannot be disabled for qsat"); ptr_vector fmls; expr_ref_vector defs(m); expr_ref fml(m);