test/regress/regress0/cores/issue4971-0.smt2

   1 ; COMMAND-LINE: --incremental -q --check-unsat-cores
   2 ; EXPECT: unknown
   3 ; EXPECT: unsat
   4 ; EXPECT: (
   5 ; EXPECT: IP_1
   6 ; EXPECT: )
   7 (declare-const v1 Bool)
   8 (declare-const v9 Bool)
   9 (declare-const v14 Bool)
  10 (declare-const i4 Int)
  11 (declare-const v16 Bool)
  12 (assert (! (forall ((q0 Bool) (q1 Bool) (q2 (_ BitVec 10)) (q3 Bool) (q4 (_ BitVec 10))) (=> (distinct (_ bv827 10) q2 q4) (xor q1 q0))) :named IP_1))
  13 (declare-const v21 Bool)
  14 (assert (! (or v9 v21 v16) :named IP_33))
  15 (assert (! (or (< (abs 404) i4) v14 v1) :named IP_51))
  16 (check-sat)
  17 (check-sat-assuming (IP_33 IP_51))
  18 (get-unsat-core)