From 602a9e3914c083aef9b089a5c05b8cf0351addfb Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 27 Sep 2022 17:55:29 +0200 Subject: [PATCH] test_l4b for another always-false constraint --- src/test/polysat.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index ee57ae689..a4a12e681 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -212,6 +212,15 @@ namespace polysat { s.expect_unsat(); } + static void test_l4b() { + scoped_solver s(__func__); + auto x = s.var(s.add_var(32)); + auto y = s.var(s.add_var(32)); + s.add_eq(2*x + 4*y + 1); // always false due to parity + s.check(); + s.expect_unsat(); + } + static void test_l5() { scoped_solver s(__func__); auto a = s.var(s.add_var(3)); @@ -1402,6 +1411,7 @@ void tst_polysat() { // test_polysat::test_l2(); // TODO: loops // test_polysat::test_l3(); // ok // test_polysat::test_l4(); // ok now (had assertion failure in conflict::insert) + // test_polysat::test_l4b(); // ok // test_polysat::test_l5(); // inefficient conflicts (needs equality reasoning) // test_polysat::test_p1(); // ok (conflict @0 by viable_fallback)