test/regress/regress0/bug1247.smt2

   1 ; COMMAND-LINE: --incremental
   2 ; EXPECT: unsat
   3 (set-logic QF_ABV)
   4 (set-info :status unsat)
   5
   6 (declare-const p Bool)
   7 (declare-const u (_ BitVec 8))
   8 (declare-const v (_ BitVec 8))
   9 (define-const t (_ BitVec 8) (ite p u v))
  10 (assert (= t #x01))
  11
  12 (push)
  13 (assert (= t #x00))
  14 (check-sat)