mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 14:55:25 +00:00
Code Activity

no recursive polysat calls

Browse source
This commit is contained in:
Jakob Rath 2023-12-22 13:22:34 +01:00
parent f111bd4de3
commit 6f93ec26ba
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -109,8 +109,7 @@ namespace polysat {
reg_decl_plugins(m); reg_decl_plugins(m);
bv = alloc(bv_util, m); bv = alloc(bv_util, m);
params_ref p; params_ref p;
p.set_bool("bv.polysat", false); p.set_uint("bv.solver", 0);
// p.set_bool("smt", true);
s = mk_solver(m, p, false, true, true, symbol::null); s = mk_solver(m, p, false, true, true, symbol::null);
m_x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width)); m_x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width));
m_x = m.mk_const(m_x_decl); m_x = m.mk_const(m_x_decl);
@ -473,8 +472,7 @@ namespace polysat {
reg_decl_plugins(m); reg_decl_plugins(m);
a = alloc(arith_util, m); a = alloc(arith_util, m);
params_ref p; params_ref p;
p.set_bool("bv.polysat", false); p.set_uint("bv.solver", 0);
// p.set_bool("smt", true);
s = mk_solver(m, p, false, true, true, symbol::null); s = mk_solver(m, p, false, true, true, symbol::null);
x_decl = m.mk_const_decl("x", a->mk_int()); x_decl = m.mk_const_decl("x", a->mk_int());
x = m.mk_const(x_decl); x = m.mk_const(x_decl);