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: Wed at 5:14 PM by petross | 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
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:
| Updated: Jul 11 at 4:06 PM by Elarnon | Created: Jul 8 at 4:23 PM by Elarnon
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:
| Updated: Jul 11 at 2:56 PM by wintersteiger | Created: Jul 8 at 4:12 PM by Elarnon
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:
| Updated: Jul 11 at 2:51 PM by wintersteiger | Created: Jul 8 at 3:51 PM by Elarnon
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:
| Updated: Jun 30 at 3:39 PM by jbridge99 | Created: Jun 30 at 3:33 PM by jbridge99
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: May 22 at 4:26 PM by NikolajBjorner | Created: May 13 at 5:33 PM by immspw
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:
| Updated: Jun 9 at 3:47 PM by wintersteiger | Created: Apr 28 at 1:02 PM by dradorf
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".
Id #105 | Release:
| Updated: May 31 at 6:49 AM by NBjorner | Created: Apr 8 at 11:30 AM by switicus