Regression

ajreynol · Dec 19, 2024 · 12f7430 · 12f7430
1 parent 19ac742
commit 12f7430
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -1324,6 +1324,7 @@ set(regress_0_tests
   regress0/proofs/dd_ic_pf_764.smt2
   regress0/proofs/dd_pf_739.smt2
   regress0/proofs/dd_spark_nnf_pf.smt2
+  regress0/proofs/dd_textbook-sumeven-arith-rcons.smt2
   regress0/proofs/define-fun-shadow.smt2
   regress0/proofs/dsl-cong-eval-cr.smt2
   regress0/proofs/dsl-no-eval.smt2

diff --git a/test/regress/cli/regress0/proofs/dd_textbook-sumeven-arith-rcons.smt2 b/test/regress/cli/regress0/proofs/dd_textbook-sumeven-arith-rcons.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun t () Int)
+(declare-fun s (Int Int Int) Int)
+(declare-fun s (Int Int Int Int Int) Int)
+(declare-fun _1 (Int Int) Int)
+(assert (and (forall ((x Int) (? Int)) (! (= 0 (_1 1 x)) :pattern ((s 0 0 x 0 ?)))) (forall ((? Int) (y Int)) (! (= (_1 0 0) (- ? (* y (_1 ? 0)))) :pattern ((_1 ? y)) :pattern ((_1 0 0))))))
+(assert (and (= 0 (_1 t 1)) (= 0 (s 0 0 2 0 (s 0 0 0)))))
+(check-sat)