Unexpected output from Z3 when verifying list.c0

[icmccorm]

Occasionally, when verifying the fully-specified version of list.c0, the following error occurs:

[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 54453 column 5: push canceled")
[info]   Cause: java.util.concurrent.ExecutionException: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 54453 column 5: push canceled")

This has only been observed when running the CompilerSpec unit test. The error isn't deterministic; usually, the test succeeds.

[icmccorm]

This also occurred during a benchmarking run with permutation #6312 of AVL, resulting in an similar error message. This permutation verifies successfully when run locally.

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 390 column 5: push canceled")

  Cause: java.util.concurrent.ExecutionException: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 390 column 5: push canceled")

[jennalwise]

Also, it seems we are not the only ones experiencing the Z3 issue: Z3Prover/z3#4713 ; it started happening from version 4.8.9 of Z3 for this person and seems to be a timeout issue with push in Z3. So, we can always increase the timeout size for Z3, which I think is a silicon option, and see if this solves the issue.