mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 11:37:54 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-06 19:00:51 -07:00
parent a1ded7f1ec
commit b5d1b0336a
3 changed files with 32 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/test/fixplex.cpp
View file

@ -54,10 +54,23 @@ namespace polysat {
fp.run();
}
static void test4() {
scoped_fp fp;
var_t x = 0, y = 1, z = 2;
var_t ys[3] = { x, y, z };
numeral coeffs[3] = { 1, 1, 1 };
fp.add_row(x, 3, ys, coeffs);
fp.set_bounds(x, 3, 4);
fp.set_bounds(y, 3, 6);
fp.run();
fp.propagate_bounds();
}
}
void tst_fixplex() {
polysat::test1();
polysat::test2();
polysat::test3();
polysat::test4();
}