O(n^4) time complexity of getConstDecls() for Enumeration Sorts in Java

The program Context ctx = new Context(); for (int sortSize = 1; sortSize < 20000; sortSize *= 2) { String[] names = new String[sortSize]; for (int i = 0; i < sortSize; i++) ...

Id #195 | Release: None | Updated: Thu at 5:31 PM by wintersteiger | Created: Tue at 4:56 PM by steimann

Feature request: switching models for multiple objective

Hi, The optimizing branch of Z3 supports multi-objective semantics, and it is possible to get a separate value for each objective. However, in the "box" mode for stacking objectives these differ...

Id #194 | Release: None | Updated: Wed at 6:53 PM by NBjorner | Created: Mon at 1:46 PM by GeorgeKarpenkov

Overflow encountered when expanding vector

Using be709802cd46a88985e481c8890db920c91e23cf from unstable, I obtain (error "line 31622 column 7: Overflow encountered when expanding vector") on the attached script

Id #193 | Release: None | Updated: Mar 22 at 2:20 PM by Heizmann | Created: Mar 22 at 2:20 PM by Heizmann

Z3 pdr fixedpoint queries return inconsistent results/ queries influence each other

I'm having a problem with inconsistent query results when using the pdr fixedpoint engine with the extended smtlib syntax in z3. It appears that queries are influencing the result of other queries,...

Id #191 | Release: None | Updated: Thu at 12:10 AM by NBjorner | Created: Mar 20 at 2:08 PM by Bluttrinker

Quantifier instantion not happening - pattern bug?

Given the program below, Z3 4.3.2 and 4.4.0 55ca6ce44b2f (both Win x64) immediately report unknown, despite the fact that the given terms and patterns should allow it to instantiate each forall onc...

Id #190 | Release: None | Updated: Tue at 10:47 AM by mschwerhoff | Created: Mar 13 at 12:02 PM by mschwerhoff

Z3_optimize_check ignores the Z3_interrupt() signal

Hi, I have a problematic case where I have a long query to Z3_optimize_check, and when I want to stop it with Z3_interrupt (coming from a different thread), my other call is ignored, and the tim...

Id #186 | Release: None | Updated: Wed at 7:30 PM by NBjorner | Created: Mar 10 at 11:26 AM by GeorgeKarpenkov

z3 segfault in mk_unit_resolution

Hi, In the OPT-branch of Z3 I get a segfault in mk_unit_resolution from the queries my tool generates. The replayable log is at http://metaworld.me/z3_segfault.log (sorry for the large size, c...

Id #185 | Release: None | Updated: Mon at 1:27 PM by wintersteiger | Created: Mar 10 at 9:39 AM by GeorgeKarpenkov

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: Mon at 1:33 PM by wintersteiger | Created: Feb 11 at 9: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: Mon at 1:32 PM by wintersteiger | Created: Feb 5 at 7:51 PM by smccamant

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 11:17 AM by wintersteiger | Created: Dec 15, 2014 at 3:01 PM by MPreiner