unknown with bit-blast

[Heaven2024]

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? :)

[NikolajBjorner]

the fp parameters are for preprocessing Horn clauses. It is used for set-logic HORN or for constrainds added by "rule' and "fact" (see the z3guide https://microsoft.github.io/z3guide/docs/fixedpoints/intro) or for constraints added using the FixedPoint context over the binary API.

[wintersteiger]

The reason you get an unknown is that the bit-blast tactic does not attempt to solve the problem, it only translates it. To solve the bit-blasted problem, you still need to call the SMT tactic, e.g. (check-sat-using (then bit-blast smt)).