1 files changed, 21 insertions, 0 deletions
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)