summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug1247.smt2
blob: e73e42fb57e35838599c84f3116d2936b0c5ac54 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14

; COMMAND-LINE: --incremental
; EXPECT: unsat
(set-logic QF_ABV)
(set-info :status unsat)

(declare-const p Bool)
(declare-const u (_ BitVec 8))
(declare-const v (_ BitVec 8))
(define-const t (_ BitVec 8) (ite p u v))
(assert (= t #x01))

(push)
(assert (= t #x00))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback