From 6d4c784ec1a536f7a961833fae767afeecd8c041 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 15 Jan 2025 16:50:40 -0600 Subject: [PATCH] More --- test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress0/datatypes/proj-issue752-ipc.smt2 | 6 ++++++ 2 files changed, 7 insertions(+) create mode 100644 test/regress/cli/regress0/datatypes/proj-issue752-ipc.smt2 diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index b0e0df062f4..e341996f1b1 100644 --- 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 new file mode 100644 index 00000000000..a2770e3b253 --- /dev/null +++ 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)))))