Supporting MWSF in Z3 API

viperproject / silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.

Mozilla Public License 2.0

79 stars 31 forks source link

Supporting MWSF in Z3 API #859

Closed marcoeilers closed 3 months ago

marcoeilers commented 3 months ago

PR #836 added Magic Wand Snapshot Functions but did not extend the Z3 API to support them. This PR adds that support.

The issue was found by @mlimbeck.

Also fixing prover options reset in test suite, which prevented the test suite from running properly with Z3 API once a Z3 option was set via an annotation once.