4 files changed, 45 insertions, 47 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)
diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am
index 751d69fe5..27487b962 100644
--- a/test/regress/regress0/uflia/Makefile.am
+++ b/test/regress/regress0/uflia/Makefile.am
@@ -40,15 +40,13 @@ SMT2_TESTS = \
 	FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \
 	stalmark_e7_27_e7_31.ec.minimized.smt2 \
 	stalmark_e7_27_e7_31.ec.smt2 \
-	tiny.smt2
+	tiny.smt2 \
+	speed2_e8_449_e8_517.ec.smt2 \
+	microwave21.ec.minimized.smt2
 #	simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
 #	javafe.ast.StandardPrettyPrint.319_no_forall.smt2
 #	javafe.ast.WhileStmt.447_no_forall.smt2
 
-# CURRENTLY FAILING:
-#	speed2_e8_449_e8_517.ec.smt2
-#	microwave21.ec.minimized.smt2
-
 # Regression tests for PL inputs
 CVC_TESTS = 
 
diff --git a/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 b/test/regress/regress0/uflia/microwave21.ec.minimized.smt2
index 0d9accb91..b37db9a1e 100644
--- a/test/regress/regress0/uflia/microwave21.ec.minimized.smt2
+++ b/test/regress/regress0/uflia/microwave21.ec.minimized.smt2
@@ -1,7 +1,7 @@
 ; initialize_defs
 ; PROPERTY DEFGEN
 (set-logic QF_UFNIA)
-(set-info :status sat)
+(set-info :status unsat)
 (declare-fun _base () Int)
 (declare-fun _n () Int)
 (assert (>= _n 0))
@@ -441,4 +441,4 @@
 ; not refinement_pass
 (assert (not (=> (= _base (- 0 1)) (and (P (- 0 1)) (P 0)))))
 (assert true)
-(check-sat)
-\ No newline at end of file
+(check-sat)