#6122·z3

Unexpected code reached in Spacer

Author: ColumpioCreated Jun 30, 2022Updated Jul 13, 2026
LabelsHorn

On the following problem:

smt2
(set-logic HORN)

(declare-fun inc (Int Int Int) Bool)
(assert (forall ((x Int) (n Int)) (inc (+ n 1) x n)))

(declare-fun inc2 (Int) Bool)
(assert (forall ((x Int)) (=> (= x 0) (inc2 x))))
(assert (forall ((x Int) (y Int) (z Int) (r1 Int) (r2 Int))
    (=> (and (inc2 x) (inc r1 y x) (inc r2 z r1)) (inc2 r2))))

(declare-fun len (Int Int) Bool)
(assert (len 0 0))
(assert (forall ((x Int) (y Int) (n Int) (r Int)) (=> (and (inc r y x) (len x n)) (len r (+ n 1)))))

(assert (forall ((x Int) (y Int)) (=> (and (inc2 x) (len x y) (= (mod y 2) 1)) false)))
(check-sat)
(get-model)

I obtain the following error:

ASSERTION VIOLATION
File: /home/z3/src/muz/spacer/spacer_convex_closure.cpp
Line: 377
UNEXPECTED CODE WAS REACHED.
4.8.18.0 84931956409ec5667e2cc9661fab0ea7f715565d z3-4.8.4-6267-g849319564