summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* renamed og to civlGravatar qadeer2015-04-22
* Better error messageGravatar akashlal2015-04-21
* added more examplesGravatar qadeer2015-04-18
* patched ghost checkingGravatar qadeer2015-04-18
* changed aux attribute to ghostGravatar qadeer2015-04-18
* fixed the treatment of externGravatar qadeer2015-04-17
* first check inGravatar qadeer2015-04-16
* patched the type checker to deal with modularityGravatar qadeer2015-04-16
* Note that CVC4 support is experimental.Gravatar Dan Liew2015-04-05
* Fix typo in README.md spotted by Jeroen Ketema.Gravatar Dan Liew2015-04-05
* Patch by Jeroen Ketema.Gravatar Dan Liew2015-04-05
* Disable test is ``Test/Secure``. They aren't set up properly.Gravatar Dan Liew2015-04-05
* Some test cases for SecureVCGen (disabled for lit currently)Gravatar akashlal2015-04-05
* VC gen for security propertiesGravatar akashlal2015-04-05
* Fix ``Test/test15/CaptureState.bpl`` test under Linux.Gravatar Dan Liew2015-04-03
* Fix ``livevars/daytona_bug2_ioctl_example_2.bpl`` test under Linux.Gravatar Dan Liew2015-04-03
* Add TravisCI build status icon to README.mdGravatar Dan Liew2015-04-03
* Clean up .gitignore fileGravatar Dan Liew2015-04-03
* Remove some old mercurial files.Gravatar Dan Liew2015-04-03
* Add .travis.yml file for TravisCI builds.Gravatar Dan Liew2015-04-03
* Add initial README.mdGravatar Dan Liew2015-04-03
* Add LICENSE file.Gravatar Dan Liew2015-04-01
* updated the example to include atomic specifications (sent by Suha)Gravatar qadeer2015-03-29
* Patch by Jeroen KetemaGravatar Dan Liew2015-03-27
* Compute MustReach information lazily, on-demandGravatar akashlal2015-03-16
* Added MustReach information to VC genGravatar akashlal2015-03-11
* If using -proverLog: make sure we flush after writing every lineGravatar Dan Liew2015-03-10
* Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188)Gravatar Dan Liew2015-03-10
* Fix bug in BigDec.FloorCeiling() which gave the wrong answers forGravatar Dan Liew2015-03-10
* fixed crash reported by Dan.Gravatar qadeer2015-03-02
* Parse Bv valuesGravatar akashlal2015-03-02
* Fix using "mkbv" as a variable name in a boogie program. This wasGravatar Dan Liew2015-02-27
* Fix using reserved Z3 keywords for real/int arithmetic operators. These are t...Gravatar Dan Liew2015-02-27
* Fix using reserved Z3 keywords for float operators. These are takenGravatar Dan Liew2015-02-27
* fix from Serdar and SuhaGravatar qadeer2015-02-24
* Merge.Gravatar Dan Liew2015-02-18
|\
* | Fix bug where some reserved Z3 keywords were not sanitizedGravatar Dan Liew2015-02-18
| * Eliminated calls to deprecated method.Gravatar wuestholz2015-02-18
| * Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.Gravatar wuestholz2015-02-18
|/
* Protect Bitvector field of BvExtractExpr when it is immutable.Gravatar Dan Liew2015-02-12
* Protect E0 and E1 in BvConcatExpr if Expr is immutable.Gravatar Dan Liew2015-02-12
* Fix what looked like a serious design issue when Type checkingGravatar Dan Liew2015-02-12
* When an Expr immutable, never change Type reference if it has been set,Gravatar Dan Liew2015-02-12
* Protect the Args field of NAryExpr when it is immutable.Gravatar Dan Liew2015-02-12
* moved some things aroundGravatar qadeer2015-02-11
* Fix performance issue in ComputeHashCode() methods of Expr classes.Gravatar Dan Liew2015-02-02
* Fix typechecking immutable Expr when we haveGravatar Dan Liew2015-01-31
* Made it produce slightly different passive commands for assignments to assump...Gravatar wuestholz2015-01-30
* Minor change to the encoding of partially verified assertions as VCGravatar wuestholz2015-01-30
* Backed out changeset ed4196d6fe50Gravatar Dan Liew2015-01-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 08:28:45 +0000