From f024fe821e05a025d197015ef170bb713db22364 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 10 Sep 2022 21:55:49 -0400 Subject: [PATCH] add regression test --- tests/sat/reg_2022-09-10.smt2 | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 tests/sat/reg_2022-09-10.smt2 diff --git a/tests/sat/reg_2022-09-10.smt2 b/tests/sat/reg_2022-09-10.smt2 new file mode 100644 index 00000000..a60368a1 --- /dev/null +++ b/tests/sat/reg_2022-09-10.smt2 @@ -0,0 +1,10 @@ + +; falsly declared unsat. minimized +; from tests/sat/QF_UF_schedule_world.2.prop1_ab_cti_max.smt2 using ddSMT . +(declare-fun p () Bool) +(declare-fun y () Bool) +(assert (= false (not p))) +(assert p) +(assert (= y p)) +(assert y) +(check-sat)