Spacer unsoundness #2641
Description
I tried the following CHC code on z3 4.7.1, and I found an unsoundness bug on the Spacer CHC solver.
(set-logic HORN)
(declare-datatypes ((Mut 1)) ((par (T) ((mut (cur T) (ret T))))))
(declare-datatypes ((List 1)) ((par (T) (nil (insert (head T) (tail (List T)))))))
(declare-fun inc&back ((List Int) (List Int) (List Int) (List Int)) Bool)
(assert (forall ((xs (List Int)))
(=> true
(inc&back nil xs nil xs))
))
(assert (forall ((x Int) (xs (List Int)) (xs! (List Int)) (rs (List Int)) (rs! (List Int)))
(=> (inc&back xs xs! rs rs!)
(inc&back (insert x xs) (insert (+ x 1) xs!) rs rs!))
))
(declare-fun length ((List Int) Int) Bool)
(assert (forall ((dummy Int))
(=> true (length nil 0))
))
(assert (forall ((n Int) (x Int) (xs (List Int)))
(=> (length xs n) (length (insert x xs) (+ 1 n)))
))
(declare-fun sum ((List Int) Int) Bool)
(assert (forall ((dummy Int))
(=> true (sum nil 0))
))
(assert (forall ((n Int) (x Int) (xs (List Int)))
(=> (sum xs n) (sum (insert x xs) (+ x n)))
))
(assert (forall ((n Int) (m Int) (l Int) (r Int) (xs (List Int)) (xs! (List Int)) (ys (List Int)) (zs (List Int)) (zs! (List Int)))
(=> (and (sum xs n) (length xs l) (sum ys m) (inc&back xs xs! zs zs!) (= zs! ys) (sum xs! r))
(= r (+ n l m)))
))
(check-sat)
(get-model)
I get the following message from z3 4.8.6.
unsat
(error "line 38 column 10: model is not available")
However the expected answer is sat, which is correctly reported by some CHC solvers such as HoIce + z3 4.7.1.
I know that current Spacer does not deal with models with inductively defined functions, but still the expected behavior is falling into timeout.