CODEWITHSUNDEEP
z3
piXel_pRo
piXel_pRo

Reputation: 159

Get UNSAT Core using Z3 from .smt2 file


I need to get unsat core from z3. The contents of .smt2 file are:
(set-option :produce-unsat-cores true) (set-logic QF_AUFBV ) (declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) ) ; Constraints (! (assert (bvslt (concat (select a (_ bv3 32) ) (concat (select a (_ bv2 32) ) (concat (select a (_ bv1 32) ) (select a (_ bv0 32) ) ) ) ) (_ bv10 32) ) ) :named ?U0) (! (assert (bvslt (_ bv10 32) (concat (select a (_ bv3 32) ) (concat (select a (_ bv2 32) ) (concat (select a (_ bv1 32) ) (select a (_ bv0 32) ) ) ) ) ) ) :named ?U1) (check-sat) (get-unsat-core) (exit)

I am getting the following output when running z3:
unsupported ; ! unsupported ; ! sat (error "line 11 column 15: unsat core is not available")
I am new to z3, can't understand what is happening here (I am sure that the expression is unsat).
Thanks.

Upvotes: 0

Views: 314

Answers (1)

dejvuth
dejvuth

Reputation: 7146

You use ! incorrectly. The exclamation point is used for naming formulae (not asserts). See section 3.9.8 from the Tutorial.

This should fix it: (assert (! (bvslt ...) :named ?U0)).

Upvotes: 1

Related Questions