llreve icon indicating copy to clipboard operation
llreve copied to clipboard

Published 20 hours ago • verified publisher icon mattulbrich

Incorrect result for swab example using Z3

Open cocreature opened this issue 8 years ago • 1 comments

Z3 returns sat here while we would expect unsat. Not yet sure what’s going on here. The generated SMT looks correct.

cocreature avatar Dec 04 '16 09:12 cocreature

This looks like a bug in Z3, I opened an issue but I leave this issue open for now.

cocreature avatar Dec 15 '16 13:12 cocreature