Hi,
I use the following Z3 version:
Z3 [version 4.3.1 - 64 bit].
When I run Z3 with the attached smt2 file, I get:
constraint not satisfied
Segmentation fault
The syntax error is at line ...
Id #40 | Release:
None
| Updated: Tue at 1:31 AM by sonertari | Created: Tue at 1:31 AM by sonertari
This patch makes z3's code work on sparcv9 processors and similar when built using gcc. It only addresses issues in the code and does not do anything about the build system (z3 is simple enough to...
Id #39 | Release:
None
| Updated: May 16 at 12:06 AM by dvitek | Created: May 16 at 12:06 AM by dvitek
Go ahead and close this bug if you don't consider Z3DEBUG && _EXTERNAL_RELEASE to be a sensible combination of build flags. We wanted to turn on assertions in z3 without turning on the various exp...
Id #38 | Release:
None
| Updated: May 15 at 11:52 PM by dvitek | Created: May 15 at 11:49 PM by dvitek
It seems like something is wrong with reference counting in ctx_simplify_tactic::imp::m_occs. Right now, when I run the Python program here:
http://es.csail.mit.edu/z3-refcount-bug.py
I get ...
Id #37 | Release:
None
| Updated: Apr 25 at 11:45 PM by nickolai | Created: Apr 25 at 11:45 PM by nickolai
There seems to be a problem with mkBVAddNoOverflow. Calling the method works, but doing any interaction with the solver results in, what seems like, an infinite loop or a crash.
I can use MkBVMul...
Id #36 | Release:
None
| Updated: Apr 20 at 9:58 PM by Beatgodes | Created: Apr 20 at 9:57 PM by Beatgodes
Hi,
We are using Z3 to prove properties of Haskell programs in our tool HipSpec. We would obviously like to use Z3 datatypes to model Haskell datatypes. The trouble is that Z3's datatypes are alg...
Id #34 | Release:
None
| Updated: Apr 10 at 3:01 PM by nick8325 | Created: Apr 9 at 10:21 PM by nick8325
Hi Leo,
Just wanted to let you know that (get-value …) has a side effect, because it permanently enables model completion. So,
(get-value (x))
(get-model)
Will report a model that is differe...
Id #31 | Release:
None
| Updated: Apr 2 at 5:09 PM by leodemoura | Created: Apr 2 at 5:09 PM by leodemoura
Suggest inclusion of a shell script doing:
ocamlfind install z3 META z3.cma z3.cmi z3.cmxa
with META containing:
description = "Z3 SMT-solver"
version = "2013-03-30"
archive(byte) = "z3.cma"...
Id #30 | Release:
None
| Updated: Apr 2 at 11:23 AM by wintersteiger | Created: Mar 30 at 9:56 AM by dmonniaux
Compiling the OCaml API yields errors.
1) Some are due to obsolete functions still being referenced from the API:
./libz3stubs.a(z3_stubs.o): In function camlidl_z3_Z3_parse_z3_string':z3_stubs.c...
Id #29 | Release:
None
| Updated: Apr 2 at 11:21 AM by wintersteiger | Created: Mar 30 at 9:33 AM by dmonniaux
I found a situation where simply performing a solver.push(); solver.pop() pair (even with nothing between) causes a later call to solver.check to return unknown rather than sat. I was able to redu...
Id #26 | Release:
None
| Updated: Mar 8 at 2:33 PM by amdragon | Created: Mar 7 at 4:56 AM by amdragon