More

ajreynol · Jan 15, 2025 · 6d4c784 · 6d4c784
1 parent 04222da
commit 6d4c784
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -734,6 +734,7 @@ set(regress_0_tests
   regress0/datatypes/proj-issue172.smt2
   regress0/datatypes/proj-issue474-app-cons-value.smt2
   regress0/datatypes/proj-issue578-clash-pf.smt2
+  regress0/datatypes/proj-issue752-ipc.smt2
   regress0/datatypes/rec1.cvc.smt2
   regress0/datatypes/rec2.cvc.smt2
   regress0/datatypes/rec4.cvc.smt2

diff --git a/test/regress/cli/regress0/datatypes/proj-issue752-ipc.smt2 b/test/regress/cli/regress0/datatypes/proj-issue752-ipc.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --produce-proofs --proof-check=eager
+; EXPECT: sat
+(set-logic QF_FFDT)
+(declare-datatypes ((d 0)) (((c (s Bool)) (_c (_s d)) (o (e Bool) (se Bool)))))
+(declare-const x d)
+(check-sat-assuming ((or ((_ is c) ((_ update e) x false)) (= x (_s x)))))