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: Wed at 5:14 PM by petross | 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

[ml-ng] Can't create recursive datatypes with ML API

The functions [Datatype.mk_constructor] and [Datatype.mk_constructor_s] both take a [Sort.sort list] as their "sorts" arguments. This prevent from creating recursive datatypes, which require NULL ...

Id #121 | Release: None | Updated: Jul 11 at 4:06 PM by Elarnon | Created: Jul 8 at 4:23 PM by Elarnon

[ml-ng] Datatype functions crash Z3

When using the ML API, using functions from the [Datatype.Constructor] module cause Z3 to segfault. This is caused by the use of the internal hash table [_sizes], whose keys are Z3 ASTs for which ...

Id #120 | Release: None | Updated: Jul 11 at 2:56 PM by wintersteiger | Created: Jul 8 at 4:12 PM by Elarnon

[ml-ng] List-returning functions crash Z3

Using the ML API with a function that returns a list of arguments (e.g. [Datatype.mk_sorts]) causes Z3 to segfault. This comes from a typo in the update_api.py script causing the ML API to write ...

Id #119 | Release: None | Updated: Jul 11 at 2:51 PM by wintersteiger | Created: Jul 8 at 3:51 PM by Elarnon

Odd behaviour X^3 vs X*X*X in Z3

Attached are two SMT2 format problem files which are identical except in one there is a term involving the variable skoRC1 ^ 3 whilst in the other this is changed to skoRC1skoRC1skoRC1. They should...

Id #118 | Release: None | Updated: Jun 30 at 3:39 PM by jbridge99 | Created: Jun 30 at 3:33 PM by jbridge99

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: May 22 at 4:26 PM by NikolajBjorner | 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