What is the problem with the specification?

What is the problem with the specification? I want to encode a model transformation system-

Id #138 | Release: None | Updated: Oct 30 at 6:45 PM by wxlfrank | Created: Oct 30 at 6:45 PM by wxlfrank

Solver gets stuck with lots of stack operations

When I do a lot of pushing and popping on the solver stack, Z3 sometimes gets stuck in an endless loop. I've isolated an example: fail.smt2 does a lot of pushing and popping, but the pattern is a...

Id #137 | Release: None | Updated: Oct 16 at 3:55 AM by NBjorner | Created: Oct 15 at 9:56 PM by henningg

Z3 crashes after fed by some instances

I downloaded the latest code from unstable branch (commit f0c63e56f338). This version of Z3 couldn't deal with these 2 instances: Instance 1: (declare-sort U 0) (declare-fun x0 () U) (declare-fun ...

Id #136 | Release: None | Updated: Oct 14 at 10:25 PM by kenmcmil | Created: Oct 9 at 11:11 AM by cxcfan

A problem in iZ3

I downloaded the source of unstable branch to do some experiments. However, I found a problem of interpolation in Z3. For a small example, I wrote a simple program which calculates the interpolant ...

Id #135 | Release: None | Updated: Oct 14 at 10:47 PM by kenmcmil | Created: Oct 6 at 2:04 PM by cxcfan

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: Oct 6 at 4:00 PM by NBjorner | Created: Oct 6 at 1: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 7:05 AM by amdragon | Created: Aug 7 at 7:05 AM by amdragon

z3 very slow with linear integer arithmetic

Hi, I'm using Z3 version "[version 4.3.1 - 64 bit]" and it seems to get stuck with this simple smt2 problem: (declare-fun x0 () Int) (declare-fun x1 () Int) (declare-fun x2 () Int) (assert (> (+ ( ...

Id #122 | Release: None | Updated: Jul 12 at 11:09 PM by wintersteiger | Created: Jul 10 at 8:49 AM by Pablo_Aledo

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 9:29 PM by Heyji | Created: May 13 at 5: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: May 31 at 6:49 AM by NBjorner | Created: Apr 8 at 11:30 AM by switicus

AUFNIRA SMT-LIB compliance bug

The following two line SMT-LIB seems to be correct according to the AUFNIRA definition. http://smtlib.cs.uiowa.edu/logics/AUFNIRA.smt2 since (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_r...

Id #90 | Release: None | Updated: Mar 24 at 10:46 PM by Heizmann | Created: Feb 13 at 5:54 PM by Heizmann