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

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

AUFNIRA SMT-LIB compliance bug

The following two line SMT-LIB seems to be correct according to the AUFNIRA definition. http://smtlib.cs.uiowa.edu/logics/AUFNIRA.smt2 since (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_r...

Id #90 | Release: None | Updated: Mar 24 at 10:46 PM by Heizmann | Created: Feb 13 at 5:54 PM by Heizmann

deadlock in free on timeout on win64

I think we're basically seeing the windows version of issue 21 here. If the timeout timer goes off while the main thread is holding a heap lock (perhaps because it is executing malloc or free), th...

Id #42 | Release: None | Updated: Jun 2, 2013 at 6:47 PM by NikolajBjorner | Created: May 29, 2013 at 5:53 PM by dvitek

timeout signal handler invokes non-signal-safe functions

On platforms where z3 uses signals to implement timeouts (anything but mac/windows), z3 has a race where it can run into problems when it invokes non-async-signal-safe functions from inside the tim...

Id #21 | Release: None | Updated: Feb 7, 2013 at 7:19 PM by dvitek | Created: Feb 6, 2013 at 5:35 PM by dvitek

  • 1-10 of 10 Work Items
    • Previous
    • 1
    • Next
    • Showing
    • 10
    • Work Items