mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-24 12:07:52 +00:00
Code Activity

looks like QF_BV is handled by inc_sat_solver

Browse source
This commit is contained in:
Jakob Rath 2022-03-10 16:19:35 +01:00
parent c648b57493
commit 4a86c3fb67
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -17,6 +17,7 @@ Author:
--*/ --*/
#include "math/polysat/univariate/univariate_solver.h" #include "math/polysat/univariate/univariate_solver.h"
#include "sat/sat_solver/inc_sat_solver.h"
#include "solver/solver.h" #include "solver/solver.h"
#include "util/util.h" #include "util/util.h"
@ -32,7 +33,7 @@ namespace polysat {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
// which concrete solver do we want here? // which concrete solver do we want here?
// need to set params to enable model and unsat core generation; and bit blasting? // need to set params to enable model and unsat core generation; and bit blasting?
s = mk_smt2_solver(m, params_ref::get_empty()); s = mk_inc_sat_solver(m, params_ref::get_empty());
} }
~univariate_bitblast_solver() override = default; ~univariate_bitblast_solver() override = default;