mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

bugbash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-03 13:13:43 -08:00
parent f5aec6ecdf
commit 3e13fe1fb2
1 changed files with 3 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/sat/smt/intblast_solver.cpp
View file

@ -200,10 +200,7 @@ namespace intblast {
m_core.reset(); m_core.reset();
m_vars.reset(); m_vars.reset();
m_is_plugin = false; m_is_plugin = false;
params_ref p(s.params()); m_solver = mk_smt2_solver(m, s.params(), symbol::null);
p.set_uint("smt.bv.solver", 0);
p.set_bool("sat.smt", false);
m_solver = mk_smt_solver(m, p, symbol::null);
for (unsigned i = 0; i < m_translate.size(); ++i) for (unsigned i = 0; i < m_translate.size(); ++i)
m_translate[i] = nullptr; m_translate[i] = nullptr;
@ -216,16 +213,9 @@ namespace intblast {
original_es.append(es); original_es.append(es);
verbose_stream() << es << "\n";
lbool r; lbool r;
if (true) { if (false) {
params_ref p; r = m_solver->check_sat(es);
p.set_uint("smt.bv.solver",0);
m_solver->updt_params(p);
r = m_solver->check_sat(es);
} }
else { else {