Datalog engine model generator potential unsoundness

[RemyCiterin]

the following smtlib2 program generate the following output on z3 4.8.17:

INPUT:

(set-logic HORN)
(declare-fun R ((_ BitVec 2) (_ BitVec 2)) Bool)
(define-fun S ((x (_ BitVec 2)) (y (_ BitVec 2))) Bool (not (= x #b10)))
(define-fun T ((i (_ BitVec 2)) (o (_ BitVec 2)) (x (_ BitVec 2)) (next@x (_ BitVec 2))) Bool (and (= i next@x) (= o (ite (bvult #b11 x) #b00 #b11))))

(assert (forall
  ((x (_ BitVec 2)) (y (_ BitVec 2)))
  (=> (= #b01 x) (R x y))
))

(assert (forall
  ((i (_ BitVec 2)) (o (_ BitVec 2)) (x (_ BitVec 2)) (next@x (_ BitVec 2)) (y (_ BitVec 2)) (next@y (_ BitVec 2)))
  (=> (and (T i o x next@x) (= i o) (R x y)) (R next@x next@y))
))

(assert (forall
  ((x (_ BitVec 2)) (y (_ BitVec 2)))
  (=> (R x y) (S x y))
))

(check-sat)

(get-model)

OUTPUT:

sat
(
  (define-fun ((x!0 (_ BitVec 2)) (x!1 (_ BitVec 2))) Bool false)
)

but this model is false because $\forall x\ y, x = 0b01 \rightarrow R\ x\ y$, and z3 on the following input return unsat

(define-fun R ((x (_ BitVec 2)) (y (_ BitVec 2))) Boo falsel)
(define-fun S ((x (_ BitVec 2)) (y (_ BitVec 2))) Bool (not (= x #b10)))
(define-fun T ((i (_ BitVec 2)) (o (_ BitVec 2)) (x (_ BitVec 2)) (next@x (_ BitVec 2))) Bool (and (= i next@x) (= o (ite (bvult #b11 x) #b00 #b11))))

(assert (forall
  ((x (_ BitVec 2)) (y (_ BitVec 2)))
  (=> (= #b01 x) (R x y))
))

(assert (forall
  ((i (_ BitVec 2)) (o (_ BitVec 2)) (x (_ BitVec 2)) (next@x (_ BitVec 2)) (y (_ BitVec 2)) (next@y (_ BitVec 2)))
  (=> (and (T i o x next@x) (= i o) (R x y)) (R next@x next@y))
))

(assert (forall
  ((x (_ BitVec 2)) (y (_ BitVec 2)))
  (=> (R x y) (S x y))
))

(check-sat)

(get-model)

[hgvk94]

What command line parameters are you using? When I run ./z3 6793.smt2 -v:1 fp.engine=spacer, I get the model

(
  (define-fun R ((x!0 (_ BitVec 2)) (x!1 (_ BitVec 2))) Bool
    (or (= x!0 #b01) (= x!0 #b11)))
)

[RemyCiterin]

I do not specify the engine

[hgvk94]

For Horn formulas over BV, Z3 does not use Spacer by default. To invoke Spacer, use the above parameter. In any case, the problem is so simple that it is solved with preprocessing.