diff options
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/crcy-si.sy | 21 |
2 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index a1fad3e3c..7f6609ea4 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1484,6 +1484,7 @@ REG1_TESTS = \ regress1/sygus/constant.sy \ regress1/sygus/constant-ite-bv.sy \ regress1/sygus/crci-ssb-unk.sy \ + regress1/sygus/crcy-si.sy \ regress1/sygus/dt-test-ns.sy \ regress1/sygus/dup-op.sy \ regress1/sygus/fg_polynomial3.sy \ diff --git a/test/regress/regress1/sygus/crcy-si.sy b/test/regress/regress1/sygus/crcy-si.sy new file mode 100644 index 000000000..46500ee4d --- /dev/null +++ b/test/regress/regress1/sygus/crcy-si.sy @@ -0,0 +1,21 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic BV) + +(define-fun Spec ((k1 Bool) (k2 Bool) (k3 Bool) ) Bool + (xor k1 (and k3 (not k2))) +) + +(synth-fun Imp ((k1 Bool) (k2 Bool) (k3 Bool)) Bool + ((Start Bool ( (and d1 d1) (or d1 d1) (xor d1 d1) (not d1) ) ) + (d1 Bool ( (and d2 d2) (or d2 d2) (xor d2 d2) (not d2) ) ) + (d2 Bool ( k1 k2 k3) ) ) +) + +(declare-var k1 Bool) +(declare-var k2 Bool) +(declare-var k3 Bool) + +(constraint (= (Spec k1 k2 k3) (Imp k1 k2 k3))) +(check-synth) |