summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
* fixed crash reported by Dan.Gravatar qadeer2015-03-02
| | | | DoModSetAnalysis needs to run before the linear and mover type checking.
* fix from Serdar and SuhaGravatar qadeer2015-02-24
|
* moved some things aroundGravatar qadeer2015-02-11
|
* minor fix to the golden fileGravatar qadeer2015-01-28
|
* added lit stuff at the top of the file and the golden outputGravatar qadeer2015-01-28
|
* Work stealing queue (PLDI '12 Vechev et al.)Gravatar Unknown2015-01-28
|
* MergeGravatar qadeer2015-01-27
|\
* | removed unused functions and axioms to make the verification fasterGravatar qadeer2015-01-27
| |
| * Worked on the verification result caching (use weights for extracted functions).Gravatar wuestholz2015-01-24
| |
| * Worked on the verification result caching (use native support for partially ↵Gravatar wuestholz2015-01-16
|/ | | | verified assertions).
* Added a test and a todo.Gravatar wuestholz2015-01-02
|
* Minor change in verification result caching (extracted functions)Gravatar wuestholz2014-12-28
|
* strengthened type checkingGravatar qadeer2014-12-26
| | | | | cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions
* changed type checking of yield procedures so that they can only call other ↵Gravatar qadeer2014-12-18
| | | | yielding procedures
* 1. made variable introduction layer explicit in the test casesGravatar qadeer2014-12-15
| | | | 2. if a single layer is specified for a global variable, that layer is the introduction layer
* patched an expected outputGravatar qadeer2014-12-15
|
* Worked on the verification result caching (extracted functions).Gravatar wuestholz2014-11-25
|
* Fixed issues in the verification result caching (old expressions).Gravatar wuestholz2014-11-24
|
* Fixed issue in the verification result caching.Gravatar wuestholz2014-11-10
|
* Worked on the verification result caching.Gravatar wuestholz2014-11-10
|
* Made it never include the statement checksum when printing assert statements.Gravatar wuestholz2014-11-16
|
* updateGravatar qadeer2014-11-14
|
* renamed :phase to :layerGravatar qadeer2014-11-14
|
* added golden outputGravatar qadeer2014-11-08
|
* more minor fix to test case houdini\testUnsatCore.bplGravatar shuvendu2014-11-07
|
* minor fix to test case houdini\testUnsatCore.bplGravatar shuvendu2014-11-07
|
* re-enabling -useUnsatCoreForContractInferGravatar shuvendu2014-11-07
| | | | An example houdini\testUnsatCore.bpl to test out the unsatCore (Currently seems to be not working)
* Worked on the verification result caching.Gravatar wuestholz2014-11-03
|
* Did some refactoring.Gravatar wuestholz2014-11-02
|
* Added a test for the verification result caching.Gravatar wuestholz2014-10-29
|
* MergeGravatar qadeer2014-10-21
|\
* | removed a useless procedureGravatar qadeer2014-10-21
| |
| * Worked on the verification result caching.Gravatar wuestholz2014-10-19
| |
| * Added more tests for the verification result caching.Gravatar wuestholz2014-10-19
| |
| * Worked on the verification result caching.Gravatar wuestholz2014-10-19
| |
| * Did some refactoring.Gravatar wuestholz2014-10-18
| |
| * Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-10-18
| |
| * Worked on the verification result caching.Gravatar wuestholz2014-10-17
| |
| * Worked on the verification result caching.Gravatar wuestholz2014-10-15
|/
* Fix issue in verification result caching for assertions without subsumption.Gravatar wuestholz2014-10-13
|
* Added a test for the issue that was fixed in changeset 'e972f163bb7c'.Gravatar wuestholz2014-09-23
|
* Add missing run lines (based off Test/doomed/runtest.bat) to doomedGravatar Dan Liew2014-09-21
| | | | | | | | tests. These are really broken because Boogie just seems to hang when they are executed. So they aren't executed right now. I'm not sure what to do with the other .bpl files. ``schaef`` left them lying around.
* more tests for houdini /inlineDepthGravatar shuvendu2014-09-19
|
* a bug fix in Houdini (also AbsHoudini)Gravatar qadeer2014-09-19
|
* additional tests for houdini /inlineDepthGravatar shuvendu2014-09-18
|
* mergeGravatar qadeer2014-08-08
|\
* | fixed codexpr bug reported by Michael Emmi; removed special handling of ↵Gravatar qadeer2014-08-08
| | | | | | | | codexpr in InjectPostConditions
| * MergeGravatar Dan Rosén2014-08-01
| |\ | |/ |/|
| * Add alpha equivalence check for Expr, and use it when lambda liftingGravatar Dan Rosén2014-08-01
| |
* | deleted the free assume about gates after parallel callsGravatar qadeer2014-07-26
|/