Regression: Lambda expression as the result of a boolean in the model

[LeventErkok]

Z3 is arguably responding "correctly" here, but this is a change in behavior; and makes the life of upstream tools rather hard when extracting models.

For this benchmark:

(set-option :produce-models true)
(set-logic ALL)
(declare-fun s0 () (Array Int Bool))
(declare-fun s1 () (Array Int Bool))
(define-fun s2 () (Array Int Bool) (store ((as const (Array Int Bool)) false) 1 true))
(assert (= s0 s2))
(assert (= s1 s2))
(define-fun b () Bool (subset s0 (complement s1)))
(check-sat)
(get-value (b))

z3 built on August 17 of 2021, produces the following nice output:

sat
((b false))

But a fresh compile of z3 from sources today produces:

sat
((b (forall ((x!1 Int)) (not (= x!1 1)))))

The response is correct, as (forall ((x!1 Int)) (not (= x!1 1))) is logically false; but it is very difficult of an upstream tool to parse and interpret this output for a call to get-value, especially when all we're looking for is a boolean value.

I'm not sure when this behavior did change, or perhaps it's tied to a configuration variable now? If so, I couldn't find anything appropriate in the z3 -pd list.

Just wanted to bring this to your attention should this be unintended. It breaks upstream tools that rely on Z3 to solve set-theoretic queries.

[NikolajBjorner]

fixed

[LeventErkok]

Thanks @NikolajBjorner. I can confirm this fixed all the tests I have regarding this functionality. Much appreciated.