summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Collapse)AuthorAge
* Use SMT2 syntax for sign_extendGravatar Michal Moskal2011-08-22
|
* deleted lazyinlining option 2 and 3Gravatar qadeer2011-08-17
| | | | fixed proc copy bounding
* fixed bug in vcgen for bitvectorsGravatar qadeer2011-07-09
|
* Don't send (check-sat) after error limit is reachedGravatar Michal Moskal2011-07-05
|
* MergeGravatar Michal Moskal2011-07-05
|\
| * Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to ↵Gravatar Unknown2011-07-05
| | | | | | | | the Z3 version to use
* | Update the RECENT_Z3 #define to include SORT_AND_ORGravatar Michal Moskal2011-06-30
| |
* | Add /T: option to Z3 to kill it if it exceeds soft timeout by more than 1sGravatar Michal Moskal2011-06-30
| |
* | SMTLib: Only use (set-logic ...) when requested; quote some more symbolsGravatar Michal Moskal2011-06-30
|/
* Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
| | | | | can lose context. Added a cache for FindLeastToVerify
* further refactoringGravatar qadeer2011-06-24
|
* fixes to z3apiGravatar qadeer2011-06-24
|
* clean up in z3apiGravatar qadeer2011-06-22
|
* various fixes to port to latest version of Microsoft.Z3.dllGravatar qadeer2011-06-22
|
* Don't set logic to UFNIA when /useArrayTheoryGravatar Michal Moskal2011-05-09
|
* Use (get-model) Z3 command; quote skolem-idsGravatar Michal Moskal2011-04-28
|
* Fix parsing of (labels) Z3 response; complain about unrecognized responses thereGravatar Michal Moskal2011-04-28
|
* Use :reason-unknown not :last-failure for Z3 in SMT mode; disable ↵Gravatar Michal Moskal2011-04-28
| | | | SORT_AND_OR option (obsolete)
* Updates for the latest changes in Z3's SMT2 parserGravatar Michal Moskal2011-04-22
|
* Test commitGravatar Michal Moskal2011-04-05
|
* Use new, SMT2 compliant, Z3 syntax for labelsGravatar MichalMoskal2011-04-02
|
* Fixed a tricky bug in z3apiGravatar akashlal2011-03-18
|
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
|
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
|
* Replaced all dictionaries that mapped to bool (i.e., were being used to ↵Gravatar mikebarnett2011-03-10
| | | | implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵Gravatar mikebarnett2011-03-10
| | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
* Added a new solution configuration, Checked, that builds the Checked ↵Gravatar mikebarnett2011-03-07
| | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
* Fix some more contracts.Gravatar mikebarnett2011-03-07
|
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
|
* Mimic Z3 logic for figuring out the blocking clause for the next counterexampleGravatar MichalMoskal2011-02-23
|
* Don't ever put a label under a quantifier.Gravatar MichalMoskal2011-02-23
|
* Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)Gravatar MichalMoskal2011-02-23
|
* Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly ↵Gravatar MichalMoskal2011-02-23
| | | | different syntax in SMT than in Simplify
* Check for timeout/memoryoutGravatar MichalMoskal2011-02-23
|
* Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq ↵Gravatar MichalMoskal2011-02-23
| | | | thing in Simplify frontend)
* Don't try to declare bv typesGravatar MichalMoskal2011-02-23
|
* Dispose of the prover when Close() is called.Gravatar MichalMoskal2011-02-23
|
* Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!)Gravatar MichalMoskal2011-02-23
|
* Pass solverargumentsGravatar MichalMoskal2011-02-23
|
* Do typed->untyped translation for -mv variablesGravatar MichalMoskal2011-02-23
|
* Provide dummy implementation of FlushAxiomsToTheoremProver()Gravatar MichalMoskal2011-02-23
|
* Fixes in /useArrayTheory handlingGravatar MichalMoskal2011-02-23
|
* Parse else-> clauses in the modelGravatar MichalMoskal2011-02-23
| | | | Disable MODEL_PARTIAL in SMTLib
* Pass :skolemid to SMTLib proverGravatar MichalMoskal2011-02-23
|
* Implement Push/Pop interface.Gravatar MichalMoskal2011-02-23
| | | | Implement ProverContext.Lookup method.
* Allow recent Z3 versions to be usedGravatar MichalMoskal2011-02-21
|
* Move model printing to ErrorModel classGravatar MichalMoskal2011-02-21
| | | | Allow construction of ErrorModel instance from Model instance
* Per SMT standard push requires an argumentGravatar MichalMoskal2011-02-21
|
* Print prover errors on stdout (same as prover warnings)Gravatar MichalMoskal2011-02-18
|
* Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3Gravatar MichalMoskal2011-02-18
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 03:22:41 +0000