search

gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Unexpected output from Z3 when verifying list.c0 #43

Open icmccorm opened 1 year ago

icmccorm commented 1 year ago

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 commented 1 year ago

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 commented 10 months ago

Also, it seems we are not the only ones experiencing the Z3 issue: https://github.com/Z3Prover/z3/issues/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.