mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-21 15:57:35 +01:00
commit f2dd95eaa9
7 changed files with 92 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/test/polysat.cpp
View file

@ -1315,9 +1315,6 @@ void tst_polysat() {
test_fi::randomized();
return;
test_polysat::test_ineq_axiom1(32, 2); // crashes
return;
// looks like a fishy conflict lemma?
test_polysat::test_monot_bounds();
return;
@ -1438,6 +1435,7 @@ void tst_polysat_argv(char** argv, int argc, int& i) {
VERIFY(parse_smt2_commands(ctx, is));
ptr_vector<expr> fmls = ctx.assertions();
polysat::scoped_solver s("polysat");
s.set_max_conflicts(1000);
g_solver = &s;
polysat::internalize(m, s, fmls);
std::cout << "checking\n";