smt.bv.enable_int2bv=false soundness bug on QF_BV formula

[muchang]

Hi,
For this formula:

(declare-fun a () Int)
(assert
 (and (distinct a 0)
 (= ((_ extract 0 0) (bvashr ((_ int2bv 3) a) ((_ int2bv 3) 1))) (_ bv0 1))
 (= 0 (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) a) ((_ int2bv 3) 7)))))))))
 (= a (bv2nat ((_ int2bv 3) a)))
 (= ((_ extract 0 0) (bvor ((_ int2bv 3) a))) (_ bv0 1))))
(check-sat)

Z3 smt.bv.enable_int2bv=false gives an incorrect answer:

[593] % z3 small.smt2
unsat
[594] % z3 smt.bv.enable_int2bv=false small.smt2
sat
[595] % 
[595] % cat small.smt2
(declare-fun a () Int)
(assert
 (and (distinct a 0)
 (= ((_ extract 0 0) (bvashr ((_ int2bv 3) a) ((_ int2bv 3) 1))) (_ bv0 1))
 (= 0 (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) a) ((_ int2bv 3) 7)))))))))
 (= a (bv2nat ((_ int2bv 3) a)))
 (= ((_ extract 0 0) (bvor ((_ int2bv 3) a))) (_ bv0 1))))
(check-sat)

OS: Ubuntu 18.04
Commit: 9be7bda

[NikolajBjorner]

sure, int2bv/bv2int are treated as uninterpreted if you disable handling them.