unstable branch does not compile

The unstable branch did not compile since a function fpa_util was named like the class fpa_util. Changed this function to fpautil. Best, Matthias and Jürgen

Id #170 | Release: None | Updated: Thu at 10:18 PM by tushar_sharma | Created: Thu at 3:35 PM by Heizmann

unstable branch does not compile

The unstable branch did not compile since a function fpa_util was named like the class fpa_util. Changed this function to fpautil. Best, Matthias and Jürgen

Id #169 | Release: None | Updated: Thu at 3:35 PM by Heizmann | Created: Thu at 3:35 PM by Heizmann

Memory leaks in the Java API

I am having similar problems as TEXT with the Java API, i.e., solver and context objects are not correctly deallocated. The following code exhibits this behavior (the same thing happens when (de)...

Id #167 | Release: None | Updated: Tue at 9:36 AM by JoergPfaehler | Created: Tue at 9:36 AM by JoergPfaehler

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

(relatively simple) optimization query times out

Hi, This time I'm actually not completely sure that it is a bug. I have a following query which times out in Z3, all variables are integers. Optimizing for (+ |main::n@3| |main::l@4|) Constrai...

Id #162 | Release: None | Updated: Thu at 10:20 AM by GeorgeKarpenkov | Created: Jan 8 at 7:18 PM by GeorgeKarpenkov

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