mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

unit test for bench 13 scenario

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-03 12:23:14 -08:00
parent 075b548089
commit db1be0f247
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/test/polysat.cpp
View file

@ -1894,6 +1894,20 @@ namespace polysat {
s.expect_sat();
}
static void test_bench13_mulovfl_ineq() {
scoped_solver s(__func__);
rational const a = rational::power_of_two(128) - 1;
rational const b = rational::power_of_two(128) - 1;
auto const x = s.var(s.add_var(256));
auto const y = s.var(s.add_var(256));
s.add_ule(-x - 1, x * y);
s.add_ule(x, a);
s.add_ule(y, b);
s.add_umul_noovfl(x, y);
s.check();
//s.expect_unsat();
}
}; // class test_polysat
@ -2028,6 +2042,7 @@ void tst_polysat() {
#if 0 // Enable this block to run a single unit test with detailed output.
collect_test_records = false;
test_max_conflicts = 50;
//test_polysat::test_bench13_mulovfl_ineq();
test_polysat::test_ineq_axiom3(32, 3); // TODO: assertion
// test_polysat::test_ineq_axiom6(32, 0); // TODO: assertion
// test_polysat::test_band5(); // TODO: assertion when clause simplification (merging p>q and p=q) is enabled