Closed
Description
Hello everyone,
I am currently working with Z3 version 4.13.0 and think that Spacer returns erroneously UNSAT for the following CHC-formula:
( set-logic HORN )
(declare-fun b ( Int ) Bool)
(declare-fun d ( Int ) Bool)
(assert (forall ( ( g Int ) ( l Bool ) ( o Int ) ) (=> (and (d o) ( = g ( ite l 1 o ) )) (d g))))
(assert (forall ( ( g Int ) ( l Bool ) ) (=> ( = g ( ite l 1 0 ) ) (d g))))
(assert (forall ( ( l Int )) (=> (>= l 1) (b (+ l 1)))))
(assert (forall ( ( g Int ) ( l Bool ) ) (=> (d g) (b g))))
(assert (=> (b (- 1)) (b 0)))
(assert (=> (b (- 1)) false))
(check-sat)
$ z3 sat.smt2
unsat
A model for the CHC system would be given by
(define-fun d ((x!0 Int)) Bool
(> x!0 (- 1)))
(define-fun b ((x!0 Int)) Bool
(> x!0 (- 1)))
Metadata
Metadata
Assignees
Labels
No labels