search

epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Test suite fails with Z3 4.6 #57

Closed romac closed 6 years ago

romac commented 6 years ago

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)
samarion commented 6 years ago

Closing as it's a duplicate of https://github.com/epfl-lara/inox/issues/32. The fix depends on having a new published version of scala-smtlib which is pending on @regb.