summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SMTLib.csproj
Commit message (Collapse)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
* Fix Boogie so it compiled with mono. Patch by Dan Liew.Gravatar Ally Donaldson2014-01-14
|
* added the QED build configurationGravatar qadeer2013-12-02
|
* cvc4 command line option & cvc4.cs in ProversGravatar pantazis2013-06-12
|
* fixed datatype bug reported by ChrisGravatar Unknown2013-03-05
| | | | fixed function body referring to globals bug
* Removed AIFramework from Boogie -- use native trivial or native ↵Gravatar boehmes2012-09-27
| | | | | | | interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
* further fixes related to using uninterpreted function for error tracesGravatar qadeer2012-02-25
| | | | removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
* Add PROVER_PATH prover option (to base options, but currently only used by ↵Gravatar Michal Moskal2011-08-29
| | | | | | SMTLib) Add support for Inspector with latest Z3/SMT2 frontend
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
|
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
|
* 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.
* Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3Gravatar MichalMoskal2011-02-18
|
* Provide /p: as the short form of /proverOpt:.Gravatar MichalMoskal2011-02-17
| | | | | Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT. Add default Z3 options when using Z3.
* Make it possible to run Z3 on pipe; use generic PROVER_LOG optionsGravatar MichalMoskal2011-02-17
|
* Start implementation of pipe communication in SMTLIB backendGravatar MichalMoskal2011-02-17
|
* Move name-quoting (already for SMT2 not SMT1) into a seprate classGravatar MichalMoskal2011-02-15
|
* Added version.cs as link to those projects that were missing itGravatar stobies2010-12-06
| | | | Select 4.0 client profile on all projects
* Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.slnGravatar qadeer2010-12-01
|
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* Update to VS2010.Gravatar MichalMoskal2010-10-07
|
* created a new build target called z3apidebug.Gravatar qadeer2010-08-29
| | | | | only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver.
* Boogie: Removed some errors with code contracts (commenting out ↵Gravatar tabarbe2010-08-27
| | | | doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
* Boogie: Changed the cce classes into one separate project, which every other ↵Gravatar tabarbe2010-08-27
| | | | project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
* Boogie: Basetypes port 3/3: Committing changed referencesGravatar tabarbe2010-08-27
| | | | Z3api.csproj shouldn't get in the way this time 'round.
* Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵Gravatar tabarbe2010-08-27
| | | | files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
* Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵Gravatar tabarbe2010-08-26
| | | | Core to jive with recent changes made to the cce class.
* Boogie: Committing changed referencesGravatar tabarbe2010-08-20
|
* Boogie: Committing changed referencesGravatar tabarbe2010-08-13
|
* Boogie: Removed cce.cs's from the provers, because they all reference ↵Gravatar tabarbe2010-07-30
| | | | projects which have a (more up-to-date) copy of cce.cs.
* Made consistent the way all of the C# projects sign themselves and include ↵Gravatar mikebarnett2010-07-30
| | | | the version information.
* Boogie: VCGeneration port part 3/3: Updating sources to reference new ↵Gravatar tabarbe2010-07-28
| | | | project; making Core work with the port by removing the nonnull requirements on one abstract method.
* Fixed reference to VCGeneration project. Mistakenly checked in project files ↵Gravatar mikebarnett2010-07-28
| | | | were pointing to the yet-to-exist C# version.
* Boogie Provers: Changed the references from binary to project references.Gravatar tabarbe2010-07-27
|
* Boogie: Committing my port of simplify, along with the slightly changed ↵Gravatar tabarbe2010-07-23
| | | | references of simplify's dependents.
* Boogie: Committing my port of the SMTLib projectGravatar tabarbe2010-07-22
|
* Boogie: Renaming the source files for the SMTLib project in preparation for ↵Gravatar tabarbe2010-07-22
commiting my port of the project.