v2.5.8

Fix test config for Boogie paths that contain spaces (#210)

v2.5.7

Add the regression of issue #203

v2.5.6

Fix lit for mac (#206)

* Fix for lit under dotnet on mac

* fixup! Fix for lit under dotnet on mac

v2.5.5

Add option /noProc:<p> to exclude procedures matching pattern <p> fro…

v2.5.2

Remove labels and unused VC generation code (#201)

* first checkin

* removed labels entirely

* removed references to Doomed
disabled doomed tests

* updated golden outputs

* disabled these tests

* updated golden outputs

* Do not parse prover options just for printing help

* calculate path only if a model exists

* check if there are prover warnings before processing model

* Revert "updated golden outputs"

This reverts commit b9e3aba64925dfb1a94770ae775b81e6b23fa6b8.

* Revert "updated golden outputs"

This reverts commit 35c39dd950591f9dc18b1c0e333dc248ca78a066.

* fixed a few golden outputs (all except the ones that use MUlTI_TRACES)

* eliminated MULTI_TRACES which was done using labels and updated golden outputs

* removed /vc: option

* remove doomed code and tests

* removed doomed related command line options

Co-authored-by: Bernhard Kragl <[email protected]>

v2.5.1

Remove deleted files from old csproj file

v2.5.0

Prover option cleanup (#197) #minor

* Remove most of the Z3 options set by default

* Remove all test runs with /typeEncoding:n

* Add list of failing/diverging tests

* fixed up line numbers
added MBQI=false in two tests where the goal is to test trigger functionality

* added MBQI=false to a bunch of tests

* updated line numbers

* Some more line number fixes

* Set nnf.sk_hack option for a specific test

* Revert elimination of /typeEncoding:n and disabling MBQI in test scripts

* Revert whitespace changes

* Disable MBQI by default

* Disable the rlimit test

Maintaining appropriate timeout values got tedious, but we keep the file
to illustrate the usage of the rlimit command-line option and attribute.

* Update some error traces

* Remove outdated notes

* Eliminate case analysis for outdated Z3 versions

* Update error trace and disable an unstable test

* Remove legacy option /z3multipleErrors (covered by /proverOpt:MULTI_TRACES)

* Remove OPTIMIZE_FOR_BV and SMTLIB2_MODEL prover options

* Ignore case (completely) in solver name

* Remove legacy /z3types option

* Remove Simplify-related options and documentation

* Rename variables to something prover independent

* Remove legacy /z3lets option

* Eliminate solver-specific top-level options and unify executable lookup

* Rename option /prover to /proverDll to better indicate its purpose

* Add option /proverHelp to print prover-specific options supported by /proverOpt

* Remove variable corresponding to legacy option

* Update documentation

* Update expected test output

Co-authored-by: Shaz Qadeer <[email protected]>

v2.4.21

Disable failing string test

v2.4.18

eliminated stratified inlining leaving along the support for stratifi…

v2.4.19

fix: Visit let-expression components consistently

Previously, the Rhss and Body are a let expression where visited in different orders in
different parts of Boogie. They are now visited consistently, always Rhss before Body.

Fixes #192