Is there any difference between Z3 2.19 and 3.2 wrt SMTLIB-2 code syntax?
After installing Z3 V3.1, the following SMT-LIB code does not work. This was fine in my previous version (Z3 V2.19).
(define-fun getIP ((o0 Int) (o1 Int) (o2 Int) (o3 Int)) BitVec[32]
(bvor (bvshl (int2bv[32] o0) (int2bv[32] 24))
(bvshl (int2bv[32] o1) (int2bv[32] 16))))
(declare-funs ((dip BitVec[32]) (m BitVec[32])))
(declare-funs ((s Bool) (d Bool) (y Int) (z Int)))
(declare-funs ((r0 Bool) (r1 Bool) (f Bool)))
(declare-funs ((r0do0 Int) (r0do1 Int) (r0do2 Int) (r0do3 Int) (r0m Int) (r0nh Int)))
(declare-funs ((r1do0 Int) (r1do1 Int) (r1do2 Int) (r1do3 Int) (r1m Int) (r1nh Int)))
(declare-funs ((fso0 Int) (fso1 Int) (fso2 Int) (fso3 Int) (fsm Int)))
(declare-funs ((fdo0 Int) (fdo1 Int) (fdo2 Int) (fdo3 Int) (fdm Int) (fp Int) (fnh Int)))
(declare-funs ((so0 Int) (so1 Int) (so2 Int) (so3 Int)))
(declare-funs ((do0 Int) (do1 Int) (do2 Int) (do3 Int)))
(assert (=> f (and (= fso0 172) (= fso1 16) (= fso2 0) (= fso3 0) (= fsm 16)
(= fdo0 150) (= fdo1 96) (= fdo2 1) (= fdo3 0) (= fdm 24)
(= fp 0))))
(assert (=> r0 (and (= r0do0 150) (= r0do1 96) (= r0do2 0) (= r0do3 0) (= r0m 16))))
(assert (=> r1 (and (= r1do0 172) (= r1do1 16) (= r1do2 0) (= r1do3 0) (= r1m 16))))
(assert (=> s (and (= so0 172) (= so1 16) (= so2 0) (= so3 1))))
(assert (=> d (and (= do0 150) (= do1 96) (= do2 1) (= do3 120))))
(assert (= m (int2bv[32] 16)))
(assert ((= dip (getIP so0 so1 so2 so3))))
(check-sat) ; sat
(model)
What do I need to change in the above code to run it in 3.1.
source to share
Z3 3.x complies with SMT 2.0 standard. There were no 2.x versions. For example, SMT 2.0 does not have a command declare-funs
; 32-bit sort (_ BitVec 32)
instead of BitVec[32]
. Z3 still supports the old incompatible SMT 2.0 parser. You just need to provide a command line option -smtc
. That being said, I suggest you switch to SMT 2.0 standard. SMT 2.0 Input Language is the official input language for the Z3. Moreover, many new functions are only available in this interface (example: parametric types).
source to share