Add missing

2 files changed, 82 insertions, 0 deletions

diff --git a/test/regress/regress0/sygus/aig-si.sy b/test/regress/regress0/sygus/aig-si.sy
new file mode 100644
index 000000000..d39184fd8
--- /dev/null
+++ b/test/regress/regress0/sygus/aig-si.sy
@@ -0,0 +1,30 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all-abort --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status
+(set-logic BV)
+
+(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+  (xor (not (xor a b)) (not (xor c d))))
+
+(synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+           ((Start Bool ((and Start Start) (not Start) a b c d))))
+
+(declare-var a Bool)
+(declare-var b Bool)
+(declare-var c Bool)
+(declare-var d Bool)
+
+(constraint
+ (= (parity a b c d) 
+    (and (AIG a b c d)
+        (not (and (and (not (and a b)) (not (and (not a) (not b))))
+               (and (not (and (not c) (not d))) (not (and c d))))))))
+
+
+(check-synth)
+
+; Solution:
+;(define-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+;(not
+;  (and
+;   (and (not (and (not a) b)) (not (and d (not c))))
+;   (and (not (and (not b) a)) (not (and (not d) c)))))) 
diff --git a/test/regress/regress0/sygus/crcy-no-si.sy b/test/regress/regress0/sygus/crcy-no-si.sy
new file mode 100644
index 000000000..b0b93cebb
--- /dev/null
+++ b/test/regress/regress0/sygus/crcy-no-si.sy
@@ -0,0 +1,52 @@
+; EXPECT: unknown
+; COMMAND-LINE: --cegqi-si=all-abort --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status
+
+(set-logic BV)
+
+
+(define-fun origCir ( (LN24 Bool) (k3 Bool) (LN237 Bool)  )  Bool    
+          (xor (not (and  LN24 k3 ) ) LN237 )
+)
+
+
+(synth-fun skel ( (LN24 Bool) (k3 Bool) (LN237 Bool)  )  Bool    
+          ((Start Bool (
+		                                  (and depth1 depth1)
+		                                  (not depth1)
+		                                  (or depth1 depth1)
+		                                  (xor depth1 depth1)
+          ))
+          (depth1 Bool (
+		                                  (and depth2 depth2)
+		                                  (not depth2)
+		                                  (or depth2 depth2)
+		                                  (xor depth2 depth2)
+          ))
+          (depth2 Bool (
+		                                  (and depth3 depth3)
+		                                  (not depth3)
+		                                  (or depth3 depth3)
+		                                  (xor depth3 depth3)
+		                                  LN237
+          ))
+          (depth3 Bool (
+		                                  (and depth4 depth4)
+		                                  (not depth4)
+		                                  (or depth4 depth4)
+		                                  (xor depth4 depth4)
+		                                  LN24
+          ))
+          (depth4 Bool (
+		                                  k3
+          )))
+)
+
+
+(declare-var LN24 Bool)
+(declare-var k3 Bool)
+(declare-var LN237 Bool)
+
+(constraint (= (origCir LN24 k3 LN237 ) (skel LN24 k3 LN237 )))
+
+
+(check-synth)