(HORN) Assertion violation at ../src/muz/spacer/spacer_context.cpp Line: 929

[muchang]

Hi,
For this formula:

(set-logic HORN)
(declare-fun a (Bool Bool Int) Bool)
(assert (forall ((b Bool) (f Bool) (g Int))
     (=> (not b) (= g 0) (a b f g))))
(assert (forall ((b Bool) (f Bool) (g Int) (c Bool) (d Int) (e Bool))
     (=> (a b f g) (= c b) e (a c e d))))
(assert (forall ((b Bool) (f Bool ))
     (=> (a b f 1) (= b f) false)))
(check-sat)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/muz/spacer/spacer_context.cpp
Line: 929
!lemma->is_ground() || is_clause(m, l)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: 9f6a733