summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
Commit message (Expand)AuthorAge
* Adding fixedpoint engine backendGravatar Ken McMillan2013-05-07
* added support for linear sets without useArrayTheory (but there is some incom...Gravatar Unknown2013-03-07
* fixed datatype bug reported by ChrisGravatar Unknown2013-03-05
* Parse integers returned by Z3 into BigNumGravatar akashlal2013-01-29
* Use the new ProverInterface's Evaluate method in stratified inlinigGravatar Unknown2013-01-03
* bug fixGravatar Unknown2012-12-28
* extended Evaluate to handle more typesGravatar Unknown2012-12-28
* Added expression evaluation APIGravatar Unknown2012-12-27
* Bug fix for ExplainHoudini. Made it robust under timeouts.Gravatar Unknown2012-12-20
* Incorporated contribution 3667, which fixes bug in /z3exe flag (http://boogie...Gravatar Rustan Leino2012-11-20
* Fix for parsing error in MAXSAT computation in ProverInterface::CheckAssumpti...Gravatar Unknown2012-10-08
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
* Implement support for alternative SMT solvers -- CVC3 and CVC4Gravatar Peter Collingbourne2012-09-06
* Made error trace generation (without labels) more general for stratifiedGravatar Unknown2012-07-04
* moved class Macro to AbsyGravatar qadeer2012-06-04
* Z3: do not assert that the ProgramFiles environment variable is setGravatar Peter Collingbourne2012-05-02
* Get Boogie and GPUVerify to compile and run with MonoGravatar Peter Collingbourne2012-05-02
* clean up in stratified inliningGravatar qadeer2012-04-29
* eliminated class ErrorModelGravatar qadeer2012-04-28
* removed proccopybounding codeGravatar qadeer2012-04-28
* removed lazy inliningGravatar qadeer2012-04-28
* various changes for using unsat cores in HoudiniGravatar qadeer2012-04-17
* small fixGravatar qadeer2012-04-04
* added nonUniformUnfolding optionGravatar qadeer2012-04-03
* deleted the option UseUnsatCoreForInliningGravatar qadeer2012-04-02
* MergeGravatar qadeer2012-04-01
|\
| * bug fix for previous refactoringGravatar Unknown2012-04-02
* | MergeGravatar qadeer2012-04-01
|\|
* | partial work on non-uniform loop unrollingGravatar qadeer2012-04-01
| * Refactored CheckAssumptions APIGravatar Unknown2012-04-02
|/
* more type checking for datatypesGravatar qadeer2012-03-18
* Cleaned up code by getting rid of ApiProverInterface.Gravatar Unknown2012-02-29
* Simplification to previous checkinGravatar Michal Moskal2012-02-28
* Introduce ApiProverInterface.CheckOutcomeCore() for stratified inlining; simp...Gravatar Michal Moskal2012-02-28
* fixed up SI to work with new error trace generationGravatar qadeer2012-02-28
* various fixes related to new error tracesGravatar qadeer2012-02-27
* further fixes related to using uninterpreted function for error tracesGravatar qadeer2012-02-25
* bug fixes related to using ControlFlowFunction instead of labelsGravatar qadeer2012-02-23
* MergeGravatar qadeer2012-02-23
|\
* | using model instead of labelsGravatar Unknown2012-02-23
| * added floating point keywords to reserved SMTwords listGravatar qadeer2012-02-20
|/
* minor fix in tracingGravatar qadeer2012-02-14
* minor bug in printing z3 path when running with /traceGravatar qadeer2012-02-09
* houdini will not request models nowGravatar qadeer2012-02-08
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
* made delegate a datatypeGravatar qadeer2011-12-30
* fixed problems with datatypesGravatar qadeer2011-12-29
* Added option of turning off model generation in SI. Can be very expensive som...Gravatar akashlal2011-11-26
* Produce unsat cores only when enabled (in stratified inlining)Gravatar Unknown2011-11-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-22 17:33:20 +0000