Assertion violation at src/muz/spacer/spacer_util.cpp:377

[wintered]

[629] % z3 small.smt2
Bad literal: (< query!0_1_n (* 2 query!0_0_n))
ASSERTION VIOLATION
File: ../src/muz/spacer/spacer_util.cpp
Line: 377
m_model.is_true(res)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[630] % 
[630] % cat small.smt2
(set-logic HORN)
(set-option :smt.phase_selection 5)
(assert (forall ((a Int) (b Int)) (and (= (* 2 a) b) (xor (distinct 0 b) (> b 0)))))
(check-sat)
[631] %

OS: Ubuntu 18.04
Commit: 799b613

[NikolajBjorner]

Relevancy propagation is on.
The literal where query!0_0_n appears is irrelevant.
So the model contains no assignment for query!0_0_n.
You could give this literal any truth value you like.

[agurfinkel]

Then everything works correctly in release mode, while the assertion is still useful in development mode to see if anything better can be done for similar cases that come from real applications.

Do you want me to close this, or hide the assertion?

[NikolajBjorner]

It is a very peculiar case: It is processing the equality

 (= (* 2 query!0_0_n) query!0_1_n)

Model evaluation determines that it is false, because query!0_1_n = 1 (even parity cannot be = 1),
but does not bind a value to query!0_0_n. Then later on it doesn't evaluate
(< (* 2 query!0_0_n) query!0_1_n)
to a definite value.

Suggestion: replace assert by:
CTRACE("spacer", !m_model.is_true(res), tout << .... << "\n";);