search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

unknown with bit-blast #7274

Open Heaven2024 opened 3 days ago

Heaven2024 commented 3 days ago

Hi! Z3 [version 4.13.1 - 64 bit] ubuntu:22.04

cat xx.smt2
(set-logic ALL)
(declare-const x (_ BitVec 2))
(declare-const y (_ BitVec 2))

(assert (bvugt (bvadd x y) (_ bv2 2)))

(check-sat-using bit-blast)
(check-sat)
(get-model)

z3 xx.smt2
unknown
sat
(
  (define-fun x () (_ BitVec 2)
    #b11)
  (define-fun y () (_ BitVec 2)
    #b00)
)

I don't know what the difference is when I set-option :fp.xform.bit_blast true it return sat as expectly. I understand they have the same effect? :)