diff options
Diffstat (limited to 'test/regress/regress0/uflia/error0.delta01.smtv1.smt2')
| -rw-r--r-- | test/regress/regress0/uflia/error0.delta01.smtv1.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/uflia/error0.delta01.smtv1.smt2 b/test/regress/regress0/uflia/error0.delta01.smtv1.smt2 new file mode 100644 index 000000000..bc2d0166c --- /dev/null +++ b/test/regress/regress0/uflia/error0.delta01.smtv1.smt2 @@ -0,0 +1,10 @@ +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_UFLIA) +(declare-fun format (Int) Int) +(declare-fun arg1 () Int) +(declare-fun fmt1 () Int) +(declare-fun s_count (Int) Int) +(declare-fun fmt0 () Int) +(declare-fun x_count (Int) Int) +(check-sat-assuming ( (let ((_let_0 (* (- 1) fmt1))) (let ((_let_1 (+ _let_0 fmt0))) (let ((_let_2 (* (- 1) (x_count 7)))) (let ((_let_3 (+ fmt1 (- 2) (* (- 1) fmt0)))) (let ((_let_4 (s_count _let_3))) (let ((_let_5 (>= (x_count 1) 0))) (and true (>= _let_1 (- 8)) (>= (+ (x_count 6) _let_2) 0) (>= fmt1 7) (<= arg1 6) (not (= 0 (+ _let_4 (* (- 1) (s_count 5))))) (<= _let_1 (- 7)) (or false false (<= (+ arg1 (* (- 1) fmt0)) 1) (<= (+ _let_0 arg1) 0)) _let_5 (<= (format 7) 0) (or false false false false false _let_5 (= 0 (+ _let_2 (x_count _let_3))) (= 0 (+ _let_4 (* (- 1) (s_count 6))))) (>= (format (+ 1 fmt1)) 0) (>= (format 4) 0) (<= (format 9) 0) (>= (format fmt1) 0) (>= (format 12) 0) (= 0 (format arg1))))))))) )) |