Interpolant do not satisfy symbol condition

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: None | Updated: Feb 22 at 1:36 AM by Heizmann | Created: Feb 22 at 1:35 AM by Heizmann

segfault in printing

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: None | Updated: Feb 11 at 10:45 AM by rgrig | Created: Feb 11 at 10:45 AM by rgrig

More poor performance with QF_FPBV SMT

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: None | Updated: Feb 6 at 7:04 PM by wintersteiger | Created: Feb 5 at 8:51 PM by smccamant

Introduction of (push) causes Z3 to not return an answer

Hi, 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. last-query-z3.s...

Id #166 | Release: None | Updated: Jan 17 at 4:18 PM by wintersteiger | Created: Jan 16 at 2:36 PM by danliew

Parser Segfault

I encountered a segmentation fault in Z3 when parsing the following smtlib2 input (already minimized with ddsmt): (set-logic QF_UFBV) (declare-fun f (( BitVec 1)) ( BitVec 1)) (assert (= ( bv0 1) (...

Id #152 | Release: None | Updated: Dec 29, 2014 at 12:17 PM by wintersteiger | Created: Dec 15, 2014 at 4:01 PM by MPreiner

Boolean variable not assigned to a constant in model

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: None | Updated: Dec 16, 2014 at 12:32 AM by NBjorner | Created: Dec 15, 2014 at 12:18 PM by henningg

Segmentation fault

Using the command z3 SMTLIB2_COMPLIANT=true -memory:1024 -smt2 -t:12000 z3SegmentationFault.smt2 the version Z3 [version 4.3.2 - 64 bit - build hashcode d548c51a984e] of z3 crashes nondeterminist...

Id #150 | Release: None | Updated: Jan 17 at 4:19 PM by wintersteiger | Created: Dec 11, 2014 at 8:54 PM by Heizmann

Extraneous Array can throw Solver off in ForAll

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 * def test(unused_sort): D = Datat...

Id #149 | Release: None | Updated: Dec 16, 2014 at 6:58 PM by wintersteiger | Created: Dec 4, 2014 at 1:22 AM by clockish

Z3 Rush Hour example: generate_explanation seg faults

Hi, 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: None | Updated: Dec 16, 2014 at 7:13 PM by wintersteiger | Created: Nov 18, 2014 at 9:01 PM by quantumlight

Trace File & Concurrency

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: None | Updated: Dec 16, 2014 at 7:12 PM by wintersteiger | Created: Oct 6, 2014 at 2:14 PM by JoergPfaehler