Problems with installing z3 java api on mac

Hi, 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 Tha...

Id #128 | Release: None | Updated: Mon at 11:43 AM by wintersteiger | Created: Aug 22 at 1:59 PM by zverlov

friend function definition in expr class: compilation error

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: None | Updated: Aug 14 at 3:42 PM by Heyji | Created: Aug 14 at 9:17 AM by Heyji

Format-string treatment of variable names

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: None | Updated: Aug 12 at 1:19 AM by AndrewGacek | Created: Aug 12 at 1:19 AM by AndrewGacek

array-ext appearing in model

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: None | Updated: Aug 7 at 7:05 AM by amdragon | Created: Aug 7 at 7:05 AM by amdragon

Z3 for Java (python scripts/mk_make.py --java)

Hi, 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: None | Updated: Jul 24 at 5:15 PM by wintersteiger | Created: Jul 18 at 4:33 PM by petross

z3 very slow with linear integer arithmetic

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: None | Updated: Jul 12 at 11:09 PM by wintersteiger | Created: Jul 10 at 8:49 AM by Pablo_Aledo

z3py missing on rise4fun

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: None | Updated: Jun 4 at 12:35 PM by wintersteiger | Created: May 21 at 12:49 PM by jmh93

Memory leaks when using Z3_mk_context_rc

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: None | Updated: Aug 14 at 9:29 PM by Heyji | Created: May 13 at 5:33 PM by immspw

wrong model returned from non-linear constraint

With the following SMT-LIB 2.0 code as input to Z3 started as z3 /smt2 non-linear.smt2 >out.txt Z3 V 4.3.0 produces sat, but a model that is wrong. (declare-var x Real) (declare-var y Real) ...

Id #108 | Release: None | Updated: Jun 9 at 3:47 PM by wintersteiger | Created: Apr 28 at 1:02 PM by dradorf

Reporting zero-valued statistics

Hi, I am processing the output of Z3 with regexs for various scripts I use to conduct experiments. I ran into a bug in my scripts today when certain inputs cause Z3 to finish "in zero time". A...

Id #105 | Release: None | Updated: May 31 at 6:49 AM by NBjorner | Created: Apr 8 at 11:30 AM by switicus