1

Closed

z3 opt: hard assertion not obeyed

description

I am attaching a script that uses optimization feature of Z3 opt branch (commit 10cdbb881f014b67fcbcc93a0e39c6ac5aee9eb1).
The model produced seem not to obey the hard assertion: (assert (or SIV@9 SIV@10)). In the model, both variables are set to false.

file attachments

Closed Jun 24, 2015 at 4:55 PM by NBjorner

comments

wintersteiger wrote Jun 24, 2015 at 4:13 PM

Z3 has moved and the codeplex issue tracker is being retired. So we don't lose track I'll close this issue here; if there is still a problem, please consider opening an issue at the new tracker here.

NBjorner wrote Jun 24, 2015 at 4:55 PM

Already reported and fixed on github.