Bug with bit-vector `sign_extend`?

[aaronbembenek]

Thanks for your great tool!

I believe I've run into a bug (using commit 1f0a06efceb46d6aa19d9cd0f945aa61fbf19d50).

I ran this command: ./eld example.smt2 -scex

where example.smt2 is:

(set-logic HORN)
(declare-fun foo ((_ BitVec 1)) Bool)
(declare-fun bar ((_ BitVec 2)) Bool)
(assert (foo (_ bv1 1)))
(assert
  (forall
    ((x (_ BitVec 1)))
    (=> (foo x) (bar ((_ sign_extend 1) x)))))
(assert
  (forall
    ((x (_ BitVec 2)))
    (=> (bar x) (= x (_ bv3 2)))))
(check-sat)
(get-model)

I got this result:

Warning: ignoring get-model
unsat

0: false -> 1
1: (bar (_ bv1 2)) -> 2
2: (foo (_ bv1 1))

However, I believe the instance is satisfiable, and line 1: of the counterexample looks wrong to me: the proposition (bar (_ bv3 2)) should hold, not the proposition (bar (_ bv1 2)). Z3 agrees with me:

sat
(
  (define-fun bar ((x!0 (_ BitVec 2))) Bool
    (= x!0 #b11))
  (define-fun foo ((x!0 (_ BitVec 1))) Bool
    (= x!0 #b1))
)

Perhaps Eldarica is doing a zero_extend instead of a sign_extend?

Thanks!

[pruemmer]

Thank you for the bug report. This is indeed incorrect behavior, the bug was introduced by a commit two weeks ago. It should be fixed in the latest master!

[aaronbembenek]

Thank you for the quick fix!