search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.22k stars 1.47k forks source link

ASSERTION VIOLATION, File: ../src/sat/sat_drat.cpp #7224

Closed fwangdo closed 4 months ago

fwangdo commented 4 months ago

Greetings, For this instance, a crash occurred. We tried to make this instance as small as possible. We sincerely hope that our report will be helpful for the z3 team.

$./z3 ./small.smt2 sat.drat.check_unsat=true
Verification of -431 -545 failed
ASSERTION VIOLATION
File: ../src/sat/sat_drat.cpp
Line: 421
UNEXPECTED CODE WAS REACHED.
Z3 4.13.1.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

$ cat ./small.smt2
(declare-fun packet () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun madebysaiyan_0 () (_ BitVec 16))
(assert (= (_ bv3 32) ((_ zero_extend 24) (select packet (_ bv240 32)))))
(assert (= (_ bv0 32) ((_ zero_extend 24) (select packet (_ bv28 32)))))
(assert (not (= (_ bv0 32) ((_ zero_extend 24) (select packet (_ bv29 32))))))
(assert (= (_ bv1 32) ((_ zero_extend 24) (select packet (_ bv242 32)))))
(assert (not (= (_ bv12 32) ((_ zero_extend 24) (select packet (bvadd (_ bv242 32) ((_ zero_extend 24) (select packet (_ bv241 32)))))))))
(assert (not (= (_ bv0 32) ((_ zero_extend 24) (select packet (bvadd (_ bv242 32) ((_ zero_extend 24) (select packet (_ bv241 32)))))))))
(assert (not (= (_ bv3 32) ((_ zero_extend 24) (select packet (bvadd (_ bv242 32) ((_ zero_extend 24) (select packet (_ bv241 32)))))))))
(assert (not (= (_ bv255 32) ((_ zero_extend 24) (select packet (bvadd (_ bv242 32) ((_ zero_extend 24) (select packet (_ bv241 32)))))))))
(assert (not (bvsle (_ bv19 32) (bvadd (_ bv2 32) (_ bv2 32) ((_ zero_extend 24) (select packet (_ bv241 32))) ((_ zero_extend 24) (select packet (bvadd (_ bv243 32) ((_ zero_extend 24) (select packet (_ bv241 32))))))))))
(assert (not (= (_ bv1 32) ((_ zero_extend 24) (select packet (bvadd (_ bv244 32) ((_ zero_extend 24) (bvnot ((_ extract 9 2) (bvand (bvmul (_ bv9096 16) (_ bv28 16)) (bvsrem (bvlshr (_ bv0 16) (_ bv0 16)) (bvsmod (_ bv47621 16) madebysaiyan_0)))))) ((_ zero_extend 24) (select packet (bvadd (_ bv243 32) ((_ zero_extend 24) (select packet (_ bv241 32))))))))))))
(assert (= (_ bv0 32) ((_ zero_extend 24) (select packet (bvadd (_ bv244 32) ((_ zero_extend 24) (select packet (_ bv241 32))) ((_ zero_extend 24) (select packet (bvadd (_ bv243 32) ((_ zero_extend 24) (select packet (_ bv241 32)))))))))))
(assert (not (bvsle (_ bv77 32) (bvadd (_ bv2 32) (_ bv2 32) (_ bv1 32) ((_ zero_extend 24) (select packet (_ bv241 32))) ((_ zero_extend 24) (select packet (bvadd (_ bv243 32) ((_ zero_extend 24) (select packet (_ bv241 32))))))))))
(assert (= (_ bv0 32) ((_ zero_extend 24) (select packet (bvadd (_ bv245 32) ((_ zero_extend 24) (select packet (_ bv241 32))) ((_ zero_extend 24) (select packet (bvadd (_ bv243 32) ((_ zero_extend 24) (select packet (_ bv241 32)))))))))))
(assert (not (bvsle (_ bv308 32) (bvadd (_ bv1 32) (_ bv1 32) (_ bv2 32) (_ bv2 32) ((_ zero_extend 24) (select packet (_ bv241 32))) ((_ zero_extend 24) (select packet (bvadd (_ bv243 32) ((_ zero_extend 24) (select packet (_ bv241 32))))))))))
(assert (= (_ bv50 32) ((_ zero_extend 24) (select packet (bvadd (_ bv246 32) ((_ zero_extend 24) (select packet (_ bv241 32))) ((_ zero_extend 24) (select packet (bvadd (_ bv243 32) ((_ zero_extend 24) (select packet (_ bv241 32)))))))))))
(assert (not (bvsle (_ bv154 32) (bvadd (_ bv1 32) (_ bv83 32) (_ bv1 32) (_ bv1 32) (_ bv1 32) (_ bv2 32) ((_ zero_extend 24) (select packet (_ bv241 32))) ((_ zero_extend 24) (select packet (bvadd (_ bv243 32) ((_ zero_extend 24) (select packet (_ bv241 32))))))))))
(assert (bvule (_ bv40304 16) madebysaiyan_0))
(check-sat)

commit version: e036a5b

NikolajBjorner commented 4 months ago

this combination of features isn's suitable. sat.drat features are for DIMACS input, not smt2. Use instead:

z3 file.smt2 solver.proof.log=log.smt2 sat.smt=true

then

z3 log.smt2

fwangdo commented 4 months ago

@NikolajBjorner Thanks for letting me know. :)