mirror of
https://github.com/Z3Prover/z3
synced 2025-06-23 06:13:40 +00:00
investigate bench4
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a6b49d8b4e
commit
e716e507d9
1 changed files with 3 additions and 0 deletions
|
@ -1635,6 +1635,7 @@ void tst_polysat() {
|
||||||
// test_polysat::test_band5_clause();
|
// test_polysat::test_band5_clause();
|
||||||
// test_polysat::test_ineq_axiom1(32, 1);
|
// test_polysat::test_ineq_axiom1(32, 1);
|
||||||
// test_polysat::test_pop_conflict();
|
// test_polysat::test_pop_conflict();
|
||||||
|
test_polysat::test_ineq_basic4();
|
||||||
// test_polysat::test_l2();
|
// test_polysat::test_l2();
|
||||||
// test_polysat::test_ineq1();
|
// test_polysat::test_ineq1();
|
||||||
test_polysat::test_ineq2();
|
test_polysat::test_ineq2();
|
||||||
|
@ -1662,6 +1663,8 @@ void tst_polysat() {
|
||||||
set_log_enabled(false);
|
set_log_enabled(false);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
return;
|
||||||
|
|
||||||
RUN(test_polysat::test_clause_simplify1());
|
RUN(test_polysat::test_clause_simplify1());
|
||||||
|
|
||||||
RUN(test_polysat::test_add_conflicts());
|
RUN(test_polysat::test_add_conflicts());
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue