Flag to check invariance of entire values in sygus explain (#1908)

1 files changed, 43 insertions, 0 deletions

diff --git a/test/regress/regress1/sygus/crci-ssb-unk.sy b/test/regress/regress1/sygus/crci-ssb-unk.sy
new file mode 100644
index 000000000..f2b28db9c
--- /dev/null
+++ b/test/regress/regress1/sygus/crci-ssb-unk.sy
@@ -0,0 +1,43 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic BV)
+
+
+(define-fun origCir ( (LN4 Bool) (LN91 Bool)  )  Bool    
+          (and  LN91 LN4 )
+)
+
+
+(synth-fun skel ( (LN4 Bool) (LN91 Bool)  )  Bool    
+          ((Start Bool (
+                                  (and depth1 depth1)
+                                  (xor depth1 depth1)
+          ))
+          (depth1 Bool (
+                                  (not depth2)
+                                  LN91
+          ))
+          (depth2 Bool (
+                                  (and depth3 depth3)
+                                  (not depth3)
+                                  (or depth3 depth3)
+          ))
+          (depth3 Bool (
+                                  (and depth4 depth4)
+                                  (not depth4)
+                                  (or depth4 depth4)
+                                  (xor depth4 depth4)
+          ))
+          (depth4 Bool (
+                                  LN4
+          )))
+)
+
+
+(declare-var LN4 Bool)
+(declare-var LN91 Bool)
+
+(constraint (= (origCir LN4 LN91 ) (skel LN4 LN91 )))
+
+(check-synth)