You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This commit was created on GitHub.com and signed with GitHub’s verified signature.
The key has expired.
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 <shaz.qadeer@gmail.com>