Error due to Z3?

[jad-hamza]

I'm using Z3 4.5.1 and getting many errors when running sbt test it:test. Is it perhaps because of some change in Z3? (It doesn't seem to be because of https://github.com/epfl-lara/inox/pull/31)

For example:

[info] - 295: flatMap is associative solvr=smt-z3-opt lucky=false check=false assum=true model=0 *** FAILED *** (85 milliseconds)
[info]   inox.package$FatalError: Unexpected error from z3 solver: line 284 column 22: unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)

[samarion]

It sounds like z3 made a change in their API. You can probably fix this by adding the string "produce-unsat-assumptions=true" to the interpreterOpts in https://github.com/epfl-lara/inox/blob/master/src/main/scala/inox/solvers/smtlib/Z3Target.scala .

I'll check it against a couple older Z3 versions to make sure this is retro-compatible.

On Thu, Jul 27, 2017 at 11:02 AM, Jad notifications@github.com wrote:

I'm using Z3 4.5.1 and getting many errors when running sbt test it:test. Is it perhaps because of some change in Z3? (It doesn't seem to be because of #31 https://github.com/epfl-lara/inox/pull/31)

For example:

[info] - 295: flatMap is associative solvr=smt-z3-opt lucky=false check=false assum=true model=0 FAILED (85 milliseconds) [info] inox.package$FatalError: Unexpected error from z3 solver: line 284 column 22: unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/inox/issues/32, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhLW0ILFmy4WJZjv-XBaefIjO3LNJks5sSFIKgaJpZM4Ok_Wk .

[samarion]

Could you please try out the fix at https://github.com/epfl-lara/inox/tree/z3-unsat-assumptions? Thanks!

[jad-hamza]

Thanks I think it's fixed, but I still get other errors when running the tests, e.g.

[info] - 133: size(x) > 0 is satisfiable solvr=smt-z3 lucky=false check=false assum=true assck=false model=0 FAILED (30 milliseconds) [info] inox.package$FatalError: Unexpected error from z3 solver: Solver encountered exception: smtlib.parser.Parser$UnexpectedTokenException: Unexpected token at position: (10, 2). Expected: []. Found: OParen

[samarion]

Hmm, this is strange. I guess I'll have to bump my version of Z3 to 4.5.1 to be able to debug this.

[jad-hamza]

Actually the problem seems to come from the emit command added for the fix; is there a way to see the file created for z3 that produces the Parser error?

[samarion]

If you give the option --debug=solver, the smt2 files will be output in the smt-sessions/ folder.

[samarion]

Have you managed to take a look at the smt files?

[jad-hamza]

Can I use this option when running sbt it:test for Inox?

[samarion]

Not so easily unfortunately. You can modify the code at https://github.com/epfl-lara/inox/blob/321e1408385d0f70ab5eb8f2855ffe159e5950cb/src/it/scala/inox/TestSuite.scala#L37 to add the option optDebug(DebugSectionSolver) to config maybe, but this will produce a huge number of smt sessions since you'll get one per test.

[jad-hamza]

I tried adding :+ Main.optDebug(Set(solvers.DebugSectionSolver) to config, and also to the Seq https://github.com/epfl-lara/inox/blob/master/src/it/scala/inox/solvers/SolvingTestSuite.scala but I don't think that produced smt-sessions folders.

"size(x) > 0 is satisfiable" is one of the test that fails (with some of the options).

[samarion]

Ah yes sorry, the code that outputs the debug looks at the reporter to determine whether debugging is enabled. You need to add the option to src/test/scala/inox/TestSilentReporter.scala as well (in the argument to the parent DefaultReporter).

[jad-hamza]

Awesome thanks, I was able to get the smt outputs. However there is no issue with the smt files, the z3 executable runs well on all of them.

I ran the tests with smt-z3-opt as the only solver, and only on the "size(x) > 0 is satisfiable" tests. I noticed that the only tests that fail are the ones with --unroll-assumptions=true.

[samarion]

Could you please post the output of the z3 executable for those tests? It seems the smtlib parser is getting an unexpected response from z3 that it doesn't know how to parse when we're asking for assumptions.

[samarion]

So I went and dug into the problem a bit more and it would seem like this might actually be a bug in scala-smtlib. It seems like the response to the command GetUnsatAssumptions() is not handled correctly by scala-smtlib.

We need to add this command to the cases in ProcessInterpreter.parseResponseOf and get @regb to publish the new version of scala-smtlib.

While we're at it, I think it would make sense to change the API of ProcessInterpreter.eval to have it throw errors instead of returning a wrapped Error SExpr to enable better debugging with the stack trace.

[jad-hamza]

Thanks! I guess that is not needed anymore, but this is the content of each smt file (for the tests mentioned above), and z3's output. http://paste.ubuntu.com/25960592/

[samarion]

Pending fix in scala-smtlib: https://github.com/regb/scala-smtlib/pull/28

[samarion]

Should now be fixed, closing issue. If someone can still reproduce this, please reopen.