Unexpected output of Z3 causes Silicon to crash

[jcp19]

Recent versions of z3 (4.8.9 and beyond) have introduced changes to the possible outputs of z3 (issue, commit 1, commit 2). Silicon does not seem to be prepared to handle them. In particular, Silicon runs fine with this file when I run it with z3 version 4.8.7 but it fails when I use it with version 4.8.9 or higher, in which case it produces the output

[info] Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 37114 column 5: canceled")
[info]   Cause: java.util.concurrent.ExecutionException: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 37114 column 5: canceled")
[info] Silicon found 1 error in 02m:53s:
[info]   [0] Interaction with Z3 (instance 03) failed: Unexpected output of Z3. Expected 'success' but found: (error "line 37114 column 5: canceled")

The provided file is large (3157 lines). I was not able to reproduce the error with smaller files.

PS: Thank you @marcoeilers for pointing out the specific changes.

[mschwerhoff]

That looks like a consequence of this Z3 issue: https://github.com/Z3Prover/z3/issues/4713. It was closed, but the comment could also be interpreted as "closed and won't fix (for now)".

AFAICS, our only current option is to stick with Z3 4.8.7.

[yanntm]

Thanks for the link visible from closed issue Z3Prover/z3#4713. , I guess I'll go with 4.8.7 too, I have the same kind of errors cropping up, it was hard to diagnose too because the sample files needed to reproduce are the bigger ones.

[pieter-bos]

I ran into this while toying with a newer z3. Do you think the proposed workaround (setting a high timeout just for push) is an option for silicon?

[mschwerhoff]

I don't see why not. Would you be willing to commit a corresponding PR? I suggest the following:

• config.scala: a suitable config option that defaults to 0/None
• Z3 via stdio: and API set timeout before push
• CVC5: do nothing, since timeout can only be set upfront

@marcoeilers Any comments?