The following quantifier elimination problem breaks z3 unstable 2014-09-11 dd62ca5eb36c2a62ee44fc5a79fc27c883de21ae.
The elimination says 'False' whereas there is an obvious satisfying assignment...
Id #130 | Release:
| Updated: Fri at 9:02 AM by dmonniaux | Created: Fri at 9:02 AM by dmonniaux
I was using Z3 as a back-end theorem prover for Boogie when I noticed the following strange behavior. I tried to verify the correctness of the following piece of code:
procedure Main(x: int)
Id #129 | Release:
| Updated: Sep 8 at 3:21 PM by fniksic | Created: Sep 8 at 3:21 PM by fniksic
i was following the steps on http://leodemoura.github.io/blog/2012/12/10/z3-for-java.html to install the instable java api for z3:
git clone https://git01.codeplex.com/z3 -b unstable
Id #128 | Release:
| Updated: Sep 1 at 11:43 AM by wintersteiger | Created: Aug 22 at 1:59 PM by zverlov
In z3++ API, a bunch of friend functions (among which ite() ) are defined within the expr class. Hence their declaration is missing and visual c++ reports unknown identifiers (compilation error).
Id #127 | Release:
| Updated: Aug 14 at 3:42 PM by Heyji | Created: Aug 14 at 9:17 AM by Heyji
It looks like Z3 is using a format-string treatment of variable names in error messages. Trying running the following file (written in SMT-LIB2 format):
(assert (= 1 %x-%x-%x-%x))
For me this resu...
Id #126 | Release:
| Updated: Aug 12 at 1:19 AM by AndrewGacek | Created: Aug 12 at 1:19 AM by AndrewGacek
The attached test case produces a model that contains array-ext applications on the latest unstable (e17af8a).
According to http://stackoverflow.com/a/17226195/2502747, array-ext should not appea...
Id #125 | Release:
| Updated: Aug 7 at 7:05 AM by amdragon | Created: Aug 7 at 7:05 AM by amdragon
When trying to generate the make file with the --java option, I get an exception "failed testing java compiler". I have set the path for JAVAC as prompted but the same thing happens. What cou...
Id #124 | Release:
| Updated: Jul 24 at 5:15 PM by wintersteiger | Created: Jul 18 at 4:33 PM by petross
Hi, I'm using Z3 version "[version 4.3.1 - 64 bit]" and it seems to get stuck with this simple smt2 problem:
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(assert (> (+ ( ...
Id #122 | Release:
| Updated: Jul 12 at 11:09 PM by wintersteiger | Created: Jul 10 at 8:49 AM by Pablo_Aledo
It seems as though the z3py tutorial on rise4fun has gone missing - all the links on the codeplex homepage take me to a list of rsise4fun projects (including Z3 with the SMT interface, which seems ...
Id #112 | Release:
| Updated: Jun 4 at 12:35 PM by wintersteiger | Created: May 21 at 12:49 PM by jmh93
Hi, I have experienced an increased memory consumption of my application which uses the Z3 library. I created a small test program (attached) to investigate this issue. Inspecting this test program...
Id #109 | Release:
| Updated: Aug 14 at 9:29 PM by Heyji | Created: May 13 at 5:33 PM by immspw