summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/bv-abstr-bug.smt2
blob: cc38075a9bddfc91d9142e5497f056669e90cce9 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

; COMMAND-LINE: --bv-abstraction --bitblast=eager
;
; BV-abstraction should not be applied
(set-logic QF_BV)
(set-info :status sat)
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)
(assert
 (or
  (and a b)
  (and c d)
 )
)
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback