2 files changed, 74 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 6dfcb922a..3c118a007 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -66,7 +66,8 @@ TESTS = commutative.sy \
         cegar1.sy \
         triv-type-mismatch-si.sy \
         nia-max-square-ns.sy \
-        strings-concat-3-args.sy
+        strings-concat-3-args.sy \
+        ccp16.lus.sy
 
 
 # sygus tests currently taking too long for make regress
diff --git a/test/regress/regress0/sygus/ccp16.lus.sy b/test/regress/regress0/sygus/ccp16.lus.sy
new file mode 100644
index 000000000..662069105
--- /dev/null
+++ b/test/regress/regress0/sygus/ccp16.lus.sy
@@ -0,0 +1,72 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic SAT)
+
+(define-fun
+  __node_init_top_0 (
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+  ) Bool
+  
+  (and (= top.usr.OK_a_0 true) top.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_top_0 (
+    (top.usr.OK_a_1 Bool)
+    (top.res.init_flag_a_1 Bool)
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+  ) Bool
+  
+  (and (= top.usr.OK_a_1 true) (not top.res.init_flag_a_1))
+)
+
+
+
+(synth-inv str_invariant(
+  (top.usr.OK Bool)
+  (top.res.init_flag Bool)
+))
+
+
+(declare-primed-var top.usr.OK Bool)
+(declare-primed-var top.res.init_flag Bool)
+
+(define-fun
+  init (
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+  ) Bool
+  
+  (and (= top.usr.OK true) top.res.init_flag)
+)
+
+(define-fun
+  trans (
+    
+    ;; Current state.
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    
+    ;; Next state.
+    (top.usr.OK! Bool)
+    (top.res.init_flag! Bool)
+  
+  ) Bool
+  
+  (and (= top.usr.OK! true) (not top.res.init_flag!))
+)
+
+(define-fun
+  prop (
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+  ) Bool
+  
+  top.usr.OK
+)
+
+(inv-constraint str_invariant init trans prop)
+
+(check-synth)