Sort error in proof

Consider the following SMT-LIB 2 problem: (set-option :produce-proofs true) (set-logic AUFLIA) (declare-sort B$ 0) (declare-sort A_set$ 0) (declare-sort A_set_set$ 0) (declare-sort A_set_set_set$ 0...

Id #206 | Release: None | Updated: Sat at 5:24 PM by blanchette | Created: Sat at 5:24 PM by blanchette

bounds seem to be ignored

When I run the following small program, I get sat, despite the fact that bounds +-2 were added via add-bounds. It looks as if the bounds were ignored. Input: ;;; ;;; add-bounds.smt2 ;;; ;;; ex...

Id #205 | Release: None | Updated: Mar 1 at 1:28 PM by wintersteiger | Created: Mar 1 at 12:29 PM by dradorf


Hi, On Ubunutu 14.04 when running the following instructions: python scripts/ cd build make sudo make install I receive this error: make: *** No rule to make targe...

Id #204 | Release: None | Updated: Dec 9, 2015 at 11:46 AM by wintersteiger | Created: Dec 9, 2015 at 8:52 AM by sajjadrsm

Segmentation errors in many versions

The attached file causes a segmentation error in the following z3 versions / hashcodes: "4.3.2","2ca14b49fe45" "4.3.2","784307fc3001" "4.3.2","5e72cf0123f6" "4.4.0","0482e7fe727c" Thanks!

Id #202 | Release: None | Updated: May 18, 2015 at 6:08 PM by cipher1024 | Created: May 12, 2015 at 11:19 PM by cipher1024

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: May 19, 2015 at 11:48 AM by wintersteiger | Created: Apr 13, 2015 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 30, 2015 at 10:45 AM by wintersteiger | Created: Apr 10, 2015 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, 2015 at 8:14 PM by cipher1024 | Created: Apr 1, 2015 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, 2015 at 2:20 PM by Heizmann | Created: Mar 22, 2015 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: May 19, 2015 at 10:56 AM by wintersteiger | Created: Mar 13, 2015 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, 2015 at 7:30 PM by NBjorner | Created: Mar 10, 2015 at 11:26 AM by GeorgeKarpenkov