search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

distinct with single argument #5899

Closed LeventErkok closed 2 years ago

LeventErkok commented 2 years ago

Looks like z3 will accept calls to distinct with just one argument, ending up with essentially no constraint on the value. Something like:

(declare-const A Int)
(declare-const B Int)
(assert (distinct A))
(check-sat)
(get-model)

But more than likely the user made a mistake by forgetting to put the second argument there.

It'd be nice if z3 actually complained about the number of arguments to distinct, requiring it to be >= 2. A straight reading of the SMTLib standard suggests that was the intention.

NikolajBjorner commented 2 years ago

Other functions also take 1 argument and have to define the unit case. In some cases this led to bugs in z3 (xnor) where it is easy to mix up the unit case. I don't see why forbidding distinct to have non-unit cases is an improvement: the converse argument could be made that since you can write (and true), (xor true) without an error message why can't you write (distinct true).

LeventErkok commented 2 years ago

I believe CVC5 complains and requires at least 2 arguments for distinct. But I agree that uniformity with xor/and etc is nice too. It's just that discrepancies between different solvers is always a source of headache. But admittedly this is a minor point.