Add some regressions. Minor.

2 files changed, 232 insertions, 1 deletions

diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am
index 0451f93da..2dff1f1da 100644
--- a/test/regress/regress1/sygus/Makefile.am
+++ b/test/regress/regress1/sygus/Makefile.am
@@ -17,7 +17,8 @@ endif
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
-	hd-sdiv.sy
+	hd-sdiv.sy \
+	stopwatch-bt.sy
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress1/sygus/stopwatch-bt.sy b/test/regress/regress1/sygus/stopwatch-bt.sy
new file mode 100644
index 000000000..016280521
--- /dev/null
+++ b/test/regress/regress1/sygus/stopwatch-bt.sy
@@ -0,0 +1,230 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+(set-logic LIA)
+
+(define-fun
+  __node_init_previous_0 (
+    (previous.usr.x@0 Int)
+    (previous.usr.y@0 Int)
+    (previous.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and (= previous.usr.y@0 0) previous.res.init_flag@0)
+)
+
+(define-fun
+  __node_trans_previous_0 (
+    (previous.usr.x@1 Int)
+    (previous.usr.y@1 Int)
+    (previous.res.init_flag@1 Bool)
+    (previous.usr.x@0 Int)
+    (previous.usr.y@0 Int)
+    (previous.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and (= previous.usr.y@1 previous.usr.x@0) (not previous.res.init_flag@1))
+)
+
+(define-fun
+  __node_init_stopwatch_0 (
+    (stopwatch.usr.toggle@0 Bool)
+    (stopwatch.usr.reset@0 Bool)
+    (stopwatch.usr.count@0 Int)
+    (stopwatch.res.init_flag@0 Bool)
+    (stopwatch.res.abs_0@0 Bool)
+    (stopwatch.impl.usr.running@0 Bool)
+    (stopwatch.res.abs_1@0 Int)
+    (stopwatch.res.inst_0@0 Bool)
+  ) Bool
+  
+  (and
+   (= stopwatch.impl.usr.running@0 (not (not stopwatch.usr.toggle@0)))
+   (=
+    stopwatch.usr.count@0
+    (ite
+     stopwatch.usr.reset@0
+     0
+     (ite
+      stopwatch.impl.usr.running@0
+      (+ stopwatch.res.abs_1@0 1)
+      stopwatch.res.abs_1@0)))
+   (= stopwatch.res.abs_0@0 (>= stopwatch.usr.count@0 0))
+   (__node_init_previous_0
+    stopwatch.usr.count@0
+    stopwatch.res.abs_1@0
+    stopwatch.res.inst_0@0)
+   stopwatch.res.init_flag@0
+   true)
+)
+
+(define-fun
+  __node_trans_stopwatch_0 (
+    (stopwatch.usr.toggle@1 Bool)
+    (stopwatch.usr.reset@1 Bool)
+    (stopwatch.usr.count@1 Int)
+    (stopwatch.res.init_flag@1 Bool)
+    (stopwatch.res.abs_0@1 Bool)
+    (stopwatch.impl.usr.running@1 Bool)
+    (stopwatch.res.abs_1@1 Int)
+    (stopwatch.res.inst_0@1 Bool)
+    (stopwatch.usr.toggle@0 Bool)
+    (stopwatch.usr.reset@0 Bool)
+    (stopwatch.usr.count@0 Int)
+    (stopwatch.res.init_flag@0 Bool)
+    (stopwatch.res.abs_0@0 Bool)
+    (stopwatch.impl.usr.running@0 Bool)
+    (stopwatch.res.abs_1@0 Int)
+    (stopwatch.res.inst_0@0 Bool)
+  ) Bool
+  
+  (and
+   (=
+    stopwatch.impl.usr.running@1
+    (not (= stopwatch.impl.usr.running@0 stopwatch.usr.toggle@1)))
+   (=
+    stopwatch.usr.count@1
+    (ite
+     stopwatch.usr.reset@1
+     0
+     (ite
+      stopwatch.impl.usr.running@1
+      (+ stopwatch.res.abs_1@1 1)
+      stopwatch.res.abs_1@1)))
+   (= stopwatch.res.abs_0@1 (>= stopwatch.usr.count@1 0))
+   (__node_trans_previous_0
+    stopwatch.usr.count@1
+    stopwatch.res.abs_1@1
+    stopwatch.res.inst_0@1
+    stopwatch.usr.count@0
+    stopwatch.res.abs_1@0
+    stopwatch.res.inst_0@0)
+   (not stopwatch.res.init_flag@1)
+   true)
+)
+
+
+
+(synth-inv str_invariant(
+  (stopwatch.usr.toggle Bool)
+  (stopwatch.usr.reset Bool)
+  (stopwatch.usr.count Int)
+  (stopwatch.res.init_flag Bool)
+  (stopwatch.res.abs_0 Bool)
+  (stopwatch.impl.usr.running Bool)
+  (stopwatch.res.abs_1 Int)
+  (stopwatch.res.inst_0 Bool)
+))
+
+
+(declare-primed-var stopwatch.usr.toggle Bool)
+(declare-primed-var stopwatch.usr.reset Bool)
+(declare-primed-var stopwatch.usr.count Int)
+(declare-primed-var stopwatch.res.init_flag Bool)
+(declare-primed-var stopwatch.res.abs_0 Bool)
+(declare-primed-var stopwatch.impl.usr.running Bool)
+(declare-primed-var stopwatch.res.abs_1 Int)
+(declare-primed-var stopwatch.res.inst_0 Bool)
+
+(define-fun
+  init (
+    (stopwatch.usr.toggle Bool)
+    (stopwatch.usr.reset Bool)
+    (stopwatch.usr.count Int)
+    (stopwatch.res.init_flag Bool)
+    (stopwatch.res.abs_0 Bool)
+    (stopwatch.impl.usr.running Bool)
+    (stopwatch.res.abs_1 Int)
+    (stopwatch.res.inst_0 Bool)
+  ) Bool
+  
+  (and
+   (= stopwatch.impl.usr.running (not (not stopwatch.usr.toggle)))
+   (=
+    stopwatch.usr.count
+    (ite
+     stopwatch.usr.reset
+     0
+     (ite
+      stopwatch.impl.usr.running
+      (+ stopwatch.res.abs_1 1)
+      stopwatch.res.abs_1)))
+   (= stopwatch.res.abs_0 (>= stopwatch.usr.count 0))
+   (__node_init_previous_0
+    stopwatch.usr.count
+    stopwatch.res.abs_1
+    stopwatch.res.inst_0)
+   stopwatch.res.init_flag
+   true)
+)
+
+(define-fun
+  trans (
+    
+    ;; Constants.
+    
+    
+    ;; Current state.
+    (stopwatch.usr.toggle Bool)
+    (stopwatch.usr.reset Bool)
+    (stopwatch.usr.count Int)
+    (stopwatch.res.init_flag Bool)
+    (stopwatch.res.abs_0 Bool)
+    (stopwatch.impl.usr.running Bool)
+    (stopwatch.res.abs_1 Int)
+    (stopwatch.res.inst_0 Bool)
+    
+    ;; Next state.
+    (stopwatch.usr.toggle! Bool)
+    (stopwatch.usr.reset! Bool)
+    (stopwatch.usr.count! Int)
+    (stopwatch.res.init_flag! Bool)
+    (stopwatch.res.abs_0! Bool)
+    (stopwatch.impl.usr.running! Bool)
+    (stopwatch.res.abs_1! Int)
+    (stopwatch.res.inst_0! Bool)
+  
+  ) Bool
+  
+  (and
+   (=
+    stopwatch.impl.usr.running!
+    (not (= stopwatch.impl.usr.running stopwatch.usr.toggle!)))
+   (=
+    stopwatch.usr.count!
+    (ite
+     stopwatch.usr.reset!
+     0
+     (ite
+      stopwatch.impl.usr.running!
+      (+ stopwatch.res.abs_1! 1)
+      stopwatch.res.abs_1!)))
+   (= stopwatch.res.abs_0! (>= stopwatch.usr.count! 0))
+   (__node_trans_previous_0
+    stopwatch.usr.count!
+    stopwatch.res.abs_1!
+    stopwatch.res.inst_0!
+    stopwatch.usr.count
+    stopwatch.res.abs_1
+    stopwatch.res.inst_0)
+   (not stopwatch.res.init_flag!)
+   true)
+)
+
+(define-fun
+  prop (
+    (stopwatch.usr.toggle Bool)
+    (stopwatch.usr.reset Bool)
+    (stopwatch.usr.count Int)
+    (stopwatch.res.init_flag Bool)
+    (stopwatch.res.abs_0 Bool)
+    (stopwatch.impl.usr.running Bool)
+    (stopwatch.res.abs_1 Int)
+    (stopwatch.res.inst_0 Bool)
+  ) Bool
+  
+  stopwatch.res.abs_0
+)
+
+(inv-constraint str_invariant init trans prop)
+
+(check-synth)