CodePlexProject Hosting for Open Source Software

1

Closed

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?

(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?

## comments

leodemoura wrote Jun 29, 2013 at 2:11 AM

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

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