New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Test suite fails with Z3 4.6 #57

Closed

romac opened this issue Dec 31, 2017 · 1 comment

Member

romac commented Dec 31, 2017

The inox test suite fails when run against Z3 4.6, as it seems like Z3 now requires explicitly enabling unsat assumption construction.

For instance:

[info] - 158: simple theorem solvr=smt-z3 lucky=true check=true assum=true assck=false model=1 *** FAILED *** (39 milliseconds)
[info]   inox.package$FatalError: Unexpected error from z3 solver: line 22 column 22: unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)

The text was updated successfully, but these errors were encountered:

Member

samarion commented Jan 2, 2018

Closing as it's a duplicate of #32.
The fix depends on having a new published version of scala-smtlib which is pending on @regb.

samarion closed this as completed

jad-hamza mentioned this issue

Tests failing with Z3 4.6.0 or newer #77

Closed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment