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

remove obsolete test case

Browse source
This commit is contained in:
Jakob Rath 2022-01-19 19:10:10 +01:00
parent fa75a9109e
commit c9b9b5f531
1 changed files with 0 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/test/polysat.cpp
View file

@ -1068,41 +1068,6 @@ public:
}
}
static void test_fi_linear4(unsigned bw = 4) {
{
scoped_solver s(__func__);
auto y = s.var(s.add_var(bw));
s.add_ule(3*y + 1, 10*y);
s.check();
s.expect_sat();
}
{
scoped_solver s(__func__);
auto y = s.var(s.add_var(bw));
s.add_ult(3*y + 1, 10*y);
s.check();
s.expect_sat();
}
{
scoped_solver s(__func__);
auto y = s.var(s.add_var(bw));
s.add_ule(y-y+8, y);
s.add_ule(y, y-y+12);
s.add_ult(9*y + 3, 7*y + 1);
s.check();
s.expect_sat();
}
{
scoped_solver s(__func__);
auto y = s.var(s.add_var(bw));
s.add_ule(y-y+8, y);
s.add_ule(y, y-y+12);
s.add_ule(9*y + 3, 7*y + 1);
s.check();
s.expect_sat();
}
}
// Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
// NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
// static void test_mixed_vars() {
@ -1345,9 +1310,6 @@ void tst_polysat() {
test_fi::randomized();
return;
test_polysat::test_fi_linear4();
return;
test_polysat::test_ineq_axiom1(32, 2); // crashes
return;