From 3e13fe1fb209a6dc36b24fe0143ff59215b0ca9e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jan 2024 13:13:43 -0800 Subject: [PATCH] bugbash Signed-off-by: Nikolaj Bjorner --- src/sat/smt/intblast_solver.cpp | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 1c6a8ef3b..7a7f7cc9c 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -200,10 +200,7 @@ namespace intblast { m_core.reset(); m_vars.reset(); m_is_plugin = false; - params_ref p(s.params()); - p.set_uint("smt.bv.solver", 0); - p.set_bool("sat.smt", false); - m_solver = mk_smt_solver(m, p, symbol::null); + m_solver = mk_smt2_solver(m, s.params(), symbol::null); for (unsigned i = 0; i < m_translate.size(); ++i) m_translate[i] = nullptr; @@ -216,16 +213,9 @@ namespace intblast { original_es.append(es); - - verbose_stream() << es << "\n"; - lbool r; - if (true) { - params_ref p; - p.set_uint("smt.bv.solver",0); - m_solver->updt_params(p); - r = m_solver->check_sat(es); - + if (false) { + r = m_solver->check_sat(es); } else {