Z3/smt2_eval_MiniSat inconsistency: QF_BV/log-slicing/bvsrem_12.smt2

[hriener]

$ smt2_eval_MiniSat QF_BV/log-slicing/bvsrem_12.smt2
[metaSMT] Instance is SAT
[z3] Instance is UNSAT

[hriener]

After delta debugging:
(set-logic QF_BV)
(declare-fun substvar_508 () (_ BitVec 12))
(declare-fun substvar_601 () (_ BitVec 8))
(declare-fun substvar_585 () (_ BitVec 12))
(declare-fun substvar_573 () (_ BitVec 1))
(declare-fun substvar_624 () (_ BitVec 8))
(declare-fun substvar_604 () (_ BitVec 16))
(declare-fun substvar_595 () (_ BitVec 2))
(declare-fun substvar_506 () (_ BitVec 12))
(declare-fun substvar_625 () (_ BitVec 8))
(declare-fun substvar_616 () (_ BitVec 16))
(declare-fun substvar_567 () (_ BitVec 2))
(declare-fun substvar_478 () (_ BitVec 4))
(declare-fun substvar_507 () (_ BitVec 12))
(declare-fun substvar_613 () (_ BitVec 16))
(declare-fun substvar_614 () (_ BitVec 16))
(declare-fun substvar_598 () (_ BitVec 4))
(declare-fun substvar_586 () (_ BitVec 12))
(declare-fun substvar_590 () (_ BitVec 12))
(declare-fun substvar_640 () (_ BitVec 1))
(declare-fun substvar_594 () (_ BitVec 12))
(declare-fun substvar_477 () (_ BitVec 4))
(declare-fun substvar_435 () (_ BitVec 12))
(declare-fun substvar_568 () (_ BitVec 2))
(declare-fun substvar_584 () (_ BitVec 12))
(declare-fun substvar_617 () (_ BitVec 16))
(declare-fun substvar_574 () (_ BitVec 1))
(declare-fun substvar_610 () (_ BitVec 12))
(assert (= substvar_508 (bvsrem substvar_506 substvar_507)))
(assert (= substvar_584 (bvor (_ bv0 12) (bvand (bvnot (_ bv0 12)) substvar_506))))
(assert (= substvar_590 (bvxor (bvxor (bvnot substvar_507) (_ bv1 12)) (_ bv0 12))))
(assert (= ((_ extract 11 11) substvar_507) ((_ extract 0 0) substvar_595)))
(assert (= substvar_595 ((_ extract 3 2) substvar_598)))
(assert (= substvar_598 ((_ extract 3 0) substvar_601)))
(assert (= substvar_601 ((_ extract 15 8) substvar_604)))
(assert (= substvar_594 ((_ extract 11 0) substvar_604)))
(assert (= substvar_585 (bvor (bvand substvar_594 substvar_590) (_ bv0 12))))
(assert (= substvar_610 (bvxor (bvxor (_ bv0 12) substvar_435) (_ bv0 12))))
(assert (= substvar_584 substvar_610))
(assert (= substvar_435 ((_ extract 11 0) substvar_614)))
(assert (= substvar_613 substvar_614))
(assert (= substvar_585 ((_ extract 11 0) substvar_617)))
(assert (= substvar_616 substvar_617))
(assert (= (_ bv0 8) (bvor (_ bv0 8) (bvand (bvnot (_ bv0 8)) ((_ extract 15 8) substvar_613)))))
(assert (= substvar_624 (bvor (_ bv0 8) (bvand substvar_625 ((_ extract 15 8) substvar_616)))))
(assert (= substvar_477 (bvor (bvand substvar_478 ((_ extract 3 0) substvar_624)) (_ bv0 4))))
(assert (= substvar_567 (bvor (_ bv0 2) (bvand substvar_568 ((_ extract 3 2) substvar_477)))))
(assert (= substvar_573 (bvand substvar_574 ((_ extract 0 0) substvar_567))))
(assert (= (bvand substvar_640 substvar_573) (_ bv1 1)))
(assert (= substvar_586 substvar_435))
(assert (not (= substvar_508 (bvor (_ bv0 12) (bvand (bvnot (_ bv0 12)) substvar_586)))))
(exit)