Using the version ece838bc802b where this bug is fixed, I obtain the interpolant
(and (= x y) (= 0 x))
on the attached script. However, the symbol x occurs not in the "B partition" of the interp...
Id #182 | Release:
| Updated: Feb 22 at 1:36 AM by Heizmann | Created: Feb 22 at 1:35 AM by Heizmann
This bug is most likely in gcc, but you might want to know about it.
I get a segfault in printing (see backtrace.txt). This happened both with master and unstable, but what I say next I tested wi...
Id #179 | Release:
| Updated: Feb 11 at 10:45 AM by rgrig | Created: Feb 11 at 10:45 AM by rgrig
It seems that I've been particularly lucky (or unlucky, depending on how you look at it) that one of the first examples I tried seems to stress a lot of different performance aspects of the new sup...
Id #178 | Release:
| Updated: Feb 6 at 7:04 PM by wintersteiger | Created: Feb 5 at 8:51 PM by smccamant
I've been experimenting with incremental solving using (push) and (pop) and I've run into a bug with Z3. Attached are two nearly identical solver queries in SMTLIBv2 format.
Id #166 | Release:
| Updated: Jan 17 at 4:18 PM by wintersteiger | Created: Jan 16 at 2:36 PM by danliew
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: Dec 29, 2014 at 12:17 PM by wintersteiger | Created: Dec 15, 2014 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: Dec 16, 2014 at 12:32 AM by NBjorner | Created: Dec 15, 2014 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: Jan 17 at 4:19 PM by wintersteiger | Created: Dec 11, 2014 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: Dec 16, 2014 at 6:58 PM by wintersteiger | Created: Dec 4, 2014 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: Dec 16, 2014 at 7:13 PM by wintersteiger | Created: Nov 18, 2014 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: Dec 16, 2014 at 7:12 PM by wintersteiger | Created: Oct 6, 2014 at 2:14 PM by JoergPfaehler