compiling z3 opt

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: None | Updated: Today at 5:14 PM by NBjorner | Created: Today at 2:58 PM by ajrmorgado

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: Wed at 8:12 PM by MPreiner | Created: Mon 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: Tue at 12:32 AM by NBjorner | Created: Mon 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: Dec 11 at 8:54 PM by Heizmann | Created: Dec 11 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: Tue at 6:58 PM by wintersteiger | Created: Dec 4 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: Tue at 7:13 PM by wintersteiger | Created: Nov 18 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: Tue at 7:12 PM by wintersteiger | Created: Oct 6 at 2:14 PM by JoergPfaehler

array-ext appearing in model

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: None | Updated: Aug 7 at 8:05 AM by amdragon | Created: Aug 7 at 8:05 AM by amdragon

Memory leaks when using Z3_mk_context_rc

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: None | Updated: Aug 14 at 10:29 PM by Heyji | Created: May 13 at 6:33 PM by immspw

Reporting zero-valued statistics

Hi, 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". A...

Id #105 | Release: None | Updated: Tue at 7:31 PM by wintersteiger | Created: Apr 8 at 12:30 PM by switicus