Hi, i have cloned z3 and cjecked out for opt as follows:
$ git clone https://git01.codeplex.com/z3
$ cd z3
$ git checkout opt
$ python scripts/mk_make.py
$ cd build
but now when i do make...
Id #154 | Release:
| Updated: Today at 5:14 PM by NBjorner | Created: Today at 2:58 PM by ajrmorgado
I encountered a segmentation fault in Z3 when parsing the following smtlib2 input (already minimized with ddsmt):
(declare-fun f (( BitVec 1)) ( BitVec 1))
(assert (= ( bv0 1) (...
Id #152 | Release:
| Updated: Wed at 8:12 PM by MPreiner | Created: Mon at 4:01 PM by MPreiner
In the attached example, the variable "pred26" gets assigned to "(= (_ as-array k!0) ((as const (Array Int Int)) 0)))" instead of a boolean constant. If you remove the assertion, this behaviour van...
Id #151 | Release:
| Updated: Tue at 12:32 AM by NBjorner | Created: Mon at 12:18 PM by henningg
Using the command
z3 SMTLIB2_COMPLIANT=true -memory:1024 -smt2 -t:12000 z3SegmentationFault.smt2
Z3 [version 4.3.2 - 64 bit - build hashcode d548c51a984e]
of z3 crashes nondeterminist...
Id #150 | Release:
| Updated: Dec 11 at 8:54 PM by Heizmann | Created: Dec 11 at 8:54 PM by Heizmann
More of a feature request than a bug report I think, but:
I'm running into a failure to quantify over a tuple containing an unused Array element.
from z3 import *
D = Datat...
Id #149 | Release:
| Updated: Tue at 6:58 PM by wintersteiger | Created: Dec 4 at 1:22 AM by clockish
I was trying out Z3's fixedpoints with the rush hour example that was posted online. However whenever I set generate_explanations=True, query would seg fault
Below is the code from Mi...
Id #142 | Release:
| Updated: Tue at 7:13 PM by wintersteiger | Created: Nov 18 at 9:01 PM by quantumlight
If I use a trace file (comandline options "trace=true" and "trace_file_name=...") and use the "check-sat-using" command with two parallel smt tactics, then the trace file is basically gibberish. I ...
Id #133 | Release:
| Updated: Tue at 7:12 PM by wintersteiger | Created: Oct 6 at 2:14 PM by JoergPfaehler
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:
| Updated: Aug 7 at 8:05 AM by amdragon | Created: Aug 7 at 8:05 AM by amdragon
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: Aug 14 at 10:29 PM by Heyji | Created: May 13 at 6:33 PM by immspw
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: Tue at 7:31 PM by wintersteiger | Created: Apr 8 at 12:30 PM by switicus