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]>
