z3opt: Z3Exception: out of memory

Hi, I am trying to solve a basic example which involves multi-objective optimization. z3opt never comes back if more then one objective functions are to be optimized: s.minimize(c(i)+c(j)+c(z))...

Id #201 | Release: None | Updated: Apr 15 at 8:51 PM by UR85 | Created: Apr 13 at 8:17 PM by UR85

Strange/Wrong result

I am testing z3 for the following problem, when I am trying to find unknown values in the model it returns me unsat. But when I am giving it exact values for the for the unknown parameters for whic...

Id #200 | Release: None | Updated: Apr 15 at 3:44 PM by wintersteiger | Created: Apr 10 at 6:17 PM by UR85

Segmentation fault and inconsistent behavior

I am using Z3 version 4.3.2 - 64 bit - build hashcode 2ca14b49fe45 When I feed the following file to Z3, I get (error "tactic failed: domain sort and parameter do not match") most of the time...

Id #196 | Release: None | Updated: Apr 1 at 8:14 PM by cipher1024 | Created: Apr 1 at 8:10 PM by cipher1024

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

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: Wed at 11:28 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: Mar 25 at 7:30 PM by NBjorner | Created: Mar 10 at 11:26 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: Mar 23 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: Mar 23 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

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