Nikolaj Bjorner

``` (get-info :reason-unknown) ``` gives some information of the source of the exception. It is probably "canceled" in your cases. Then a debugger can be used to trace where/what exceptions...

Hello! For the instance ``` (set-logic HORN) (declare-fun P1 (Int Bool) Bool) (declare-fun P2 (Int Bool) Bool) (declare-fun P3 (Int Int) Bool) (declare-fun P4 (Int) Bool) (declare-fun P5 (Int) Bool)...

Hello, For the instance ``` (set-logic HORN) (declare-fun P1 (Int Int Int) Bool) (declare-fun P2 (Int) Bool) (declare-fun P3 (Int Int Int) Bool) (declare-fun P4 (Int Int Int Int Int...

Hello, For instance ``` (set-logic HORN) (declare-fun P (Int) Bool) (declare-fun Q (Bool Int Int Bool Int Int) Bool) (declare-fun R (Bool Int Int) Bool) (assert (not (exists ((v1 Int))...

Hello! For the instance ``` (set-logic HORN) (set-option :fp.xform.inline_linear_branch true) (set-option :fp.xform.inline_eager false) (declare-fun P1 (Int Int) Bool) (declare-fun P2 (Int Int Int) Bool) (declare-fun P3 (Int) Bool) (declare-fun P4...

b1606487f08cec8d950be078ac31881fc36a7bea

This is a place where z3 falls back to a generic optimization loop: ``` (define-fun cost-of-number ((t Type)) Int (ite ((_ is int) t) (bv2nat (int-bytes t)) (ite (= float...

Consider encodings of this form: ``` (assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_ bv1 4))) :weight 1) (assert-soft (=> ((_ is int) t6) (bvult (int-bytes t6) (_...

The performance regression introduced by b1606487f08cec8d950be078ac31881fc36a7bea was fixed earlier this week. It is orthogonal to the difference between arith.solver=2 and arith.solver=6. There is indeed a noticeable difference.

I am relabeling the bug because it is the same example.