1

Closed

unknown/invalid extract application error

description

I ran z3 on the attached file, and I got "unknown" when I used 4.3.2 version (z3-4.3.2.0d2a7f922c82-x64-ubuntu-12.04) and "invalid extract application" when I used 4.1 version. Surprisingly, if I added 2 extra assertions:

(assert (= (_ bv0 9) mem_13_v1))
(assert (= (_ bv0 9) mem_24_v0))

z3 will return SAT.

Is this a bug in z3? If yes, can this bug be fixed soon? My project is heavily rely on z3.

If not, can anyone point me out what I did wrong? Is it the case that these extra assertions guide the solver to prune out some space that leads to error? That's why it doesn't fail when having these assertions. If that's the case, what does that error corresponding to?

file attachments

Closed Jun 29, 2013 at 2:23 AM by leodemoura
Fixed in the unstable branch

comments

leodemoura wrote Jun 29, 2013 at 2:11 AM

The problem is that your file contains bit-vectors of size 0.
Example:
(_ bv0 0)

After I replace, (concat (_ bv0 0) i) with i
and (concat (_ bv0 0) ele) with ele
The problem goes away.

Anyway, I will add code to Z3 to report an error when bit-vectors of size zero are used.

Thanks,
Leo

leodemoura wrote Jun 29, 2013 at 2:23 AM

Quick note:

The SMT-LIB standard does not allow bit-vectors of size zero.
http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2

I added code for reporting an error when a bit-vector constant of size zero is used.
https://z3.codeplex.com/SourceControl/changeset/d9941c0ccc871881d4bbc1625bfdc005d4618ae8

mangpo wrote Jun 29, 2013 at 2:46 AM

I see. Thank you so much!