summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/qbv-simp.smt2
blob: 2bdc2d994e341dbb6c0fed2fca856e291339ab55 (plain) 
1
2
3
4
5
6
7
8
9
10
11

; COMMAND-LINE: --cegqi-bv --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
(assert
   (forall
    ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8)))
      (or (and (= A B) (= C D)) (and (= A C) (= B D)))))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback