diff options
Diffstat (limited to 'test/regress/regress0/push-pop/bug394.smt2')
| -rw-r--r-- | test/regress/regress0/push-pop/bug394.smt2 | 72 |
1 files changed, 36 insertions, 36 deletions
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)
|