summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Expand)AuthorAge
* Boogie: Added boolean code expressions (sans well-formedness checks on the in...Gravatar rustanleino2010-08-10
* Boogie: Fixed a few line endingsGravatar tabarbe2010-08-06
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
* Fixed bug in translation of select/store arguments that are BooleanGravatar qadeer2010-04-20
* First cut of lazy inlining. The option can be turned on by the flag /lazyInl...Gravatar qadeer2010-04-17
* Boogie:Gravatar rustanleino2010-02-20
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
* * Added "deprecated" comment in help message about /interprocInfer switch. T...Gravatar rustanleino2010-02-18
* 1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a linea...Gravatar qadeer2010-02-16
* Boogie: Peephole optimization to reduce depth of formulas created during VC ...Gravatar rustanleino2010-02-15
* Implemented the command line switch /useArrayTheory. This switch should be u...Gravatar qadeer2010-01-21
* Evidently, Z3 does not like QID's to start with a digit. If a Boogie filenam...Gravatar rustanleino2009-10-14
* Added /z3lets switch, which governs which kinds of LET expressions are sent t...Gravatar rustanleino2009-10-04
* Fixed some bugs in the generation of bitvector input for Z3.Gravatar rustanleino2009-09-29
* Use type-erased result type to make decision about whether or not to include ...Gravatar rustanleino2009-09-27
* Added antecedent to select-of-store axioms to make them sound even when trigg...Gravatar rustanleino2009-09-24
* Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other bit...Gravatar stobies2009-09-07
* Sign assembliesGravatar stobies2009-08-17
* Made trigger more liberal for int_2_U U_2_int axiom.Gravatar rustanleino2009-07-30
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 01:00:43 +0000