2 files changed, 40 insertions, 40 deletions
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 0af49ee1a..ca86f920d 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -30,14 +30,14 @@ SMT2_TESTS = \
 BUG_TESTS = \
 	bug216.smt2 \
 	bug233.cvc \
-	bug326.smt2
+	bug326.smt2 \
+	bug394.smt2 \
+	bug396.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
-	bug216.smt2.expect \
-	bug394.smt2 \
-	bug396.smt2
+	bug216.smt2.expect
 
 # synonyms for "check" in this directory
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/push-pop/bug394.smt2 b/test/regress/regress0/push-pop/bug394.smt2
index 5b045812d..38e59be4f 100644
--- a/test/regress/regress0/push-pop/bug394.smt2
+++ b/test/regress/regress0/push-pop/bug394.smt2
@@ -1,7 +1,7 @@
 ;(set-option :produce-unsat-cores true)
 (set-option :print-success false)
 (set-info :smt-lib-version 2.0)
-(set-option :produce-models true)
+;(set-option :produce-models true)
 (set-logic ALL_SUPPORTED)
 ; done setting options
 
@@ -1500,9 +1500,9 @@ _b44
 _b45) $getIdx)
 ))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 9318)))
-(get-value ((ControlFlow 0 823)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 9318)))
+;(get-value ((ControlFlow 0 823)))
 (assert (not (= (ControlFlow 0 823) (- 10729))))
 (check-sat)
 (pop 1)
@@ -1613,34 +1613,34 @@ _b44
 _b45) $DCT)
 ))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 11167)))
-(get-value ((ControlFlow 0 4117)))
-(get-value ((ControlFlow 0 4199)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 11167)))
+;(get-value ((ControlFlow 0 4117)))
+;(get-value ((ControlFlow 0 4199)))
 (assert (not (= (ControlFlow 0 4199) (- 13495))))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 11167)))
-(get-value ((ControlFlow 0 4117)))
-(get-value ((ControlFlow 0 4199)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 11167)))
+;(get-value ((ControlFlow 0 4117)))
+;(get-value ((ControlFlow 0 4199)))
 (assert (not (= (ControlFlow 0 4199) (- 13487))))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 11167)))
-(get-value ((ControlFlow 0 4117)))
-(get-value ((ControlFlow 0 4199)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 11167)))
+;(get-value ((ControlFlow 0 4117)))
+;(get-value ((ControlFlow 0 4199)))
 (assert (not (= (ControlFlow 0 4199) (- 13509))))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 11167)))
-(get-value ((ControlFlow 0 4117)))
-(get-value ((ControlFlow 0 4199)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 11167)))
+;(get-value ((ControlFlow 0 4117)))
+;(get-value ((ControlFlow 0 4199)))
 (assert (not (= (ControlFlow 0 4199) (- 13553))))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 11167)))
-(get-value ((ControlFlow 0 4117)))
-(get-value ((ControlFlow 0 4199)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 11167)))
+;(get-value ((ControlFlow 0 4117)))
+;(get-value ((ControlFlow 0 4199)))
 (pop 1)
 (push 1)
 (set-info :boogie-vc-id $DCT)
@@ -1695,21 +1695,21 @@ _b44
 _b45) $DCT)
 ))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 11167)))
-(get-value ((ControlFlow 0 4117)))
-(get-value ((ControlFlow 0 4199)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 11167)))
+;(get-value ((ControlFlow 0 4117)))
+;(get-value ((ControlFlow 0 4199)))
 (assert (not (= (ControlFlow 0 4199) (- 13575))))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 11167)))
-(get-value ((ControlFlow 0 4117)))
-(get-value ((ControlFlow 0 4199)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 11167)))
+;(get-value ((ControlFlow 0 4117)))
+;(get-value ((ControlFlow 0 4199)))
 (assert (not (= (ControlFlow 0 4199) (- 13712))))
 (check-sat)
-(get-value ((ControlFlow 0 0)))
-(get-value ((ControlFlow 0 11167)))
-(get-value ((ControlFlow 0 4117)))
-(get-value ((ControlFlow 0 4199)))
+;(get-value ((ControlFlow 0 0)))
+;(get-value ((ControlFlow 0 11167)))
+;(get-value ((ControlFlow 0 4117)))
+;(get-value ((ControlFlow 0 4199)))
 (assert (not (= (ControlFlow 0 4199) (- 13700))))
 (check-sat)