blob: 25bbd34d8debde7d0da12f19bf3619c7f1f3c284 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
; COMMAND-LINE: --strings-exp
;EXPECT: unsat
(set-logic ALL)
(declare-fun tickleBool (Bool) Bool)
(assert (and (tickleBool true) (tickleBool false)))
(declare-fun ControlFlow (Int Int) Int)
(declare-fun s@0 () (Seq Int))
(declare-fun s@1 () (Seq Int))
(declare-fun s@2 () (Seq Int))
(assert (not
(=> (= (ControlFlow 0 0) 170) (let ((anon0_correct (=> (= s@0 (seq.++ (as seq.empty (Seq Int)) (seq.unit 0))) (=> (and (= s@1 (seq.++ s@0 (seq.unit 1))) (= s@2 (seq.++ s@1 (seq.unit 2)))) (and (=> (= (ControlFlow 0 135) (- 0 217)) (= (seq.len s@2) 3)) (=> (= (seq.len s@2) 3) (=> (= (ControlFlow 0 135) (- 0 224)) (= (seq.extract s@2 1 2) (seq.++ (seq.unit 1) (seq.unit 2))))))))))
(let ((PreconditionGeneratedEntry_correct (=> (= (ControlFlow 0 170) 135) anon0_correct)))
PreconditionGeneratedEntry_correct)))
))
(check-sat)
|
