Unexpected code reached in Spacer
Author: ColumpioCreated Jun 30, 2022Updated Jul 13, 2026
LabelsHorn
On the following problem:
(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-g849319564Source: Z3Prover/z3