index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
/
Provers
/
SMTLib
/
Z3.cs
Commit message (
Expand
)
Author
Age
*
Merge duality changes to mainline
Ken McMillan
2013-11-09
|
\
|
*
handling timeouts for fixedpoint engines
Ken McMillan
2013-11-09
*
|
Reverted change to use MODEL_ON_FINAL_CHECK, which seems to cause Z3 unexpect...
Rustan Leino
2013-08-02
*
|
Turned on options in Z3 to try producing models for timeouts.
wuestholz
2013-08-02
*
|
refactoring and fixes in the SMTLIB2 parser
Pantazis Deligiannis
2013-07-19
*
|
added specific command line options to enable the SMTLIB2 output model parser...
Pantazis Deligiannis
2013-07-09
*
|
merge
Pantazis Deligiannis
2013-07-06
|
\
\
|
*
|
Worked on the parallelization.
wuestholz
2013-07-02
|
|
/
|
*
Fixes for duality under corral
Ken McMillan
2013-06-14
*
|
Z3 new parser takes now a new option for pp-bv-literals
pantazis
2013-06-12
|
/
*
Getting fixed point backend to work with Corral.
Ken McMillan
2013-05-29
*
Adding fixedpoint engine backend
Ken McMillan
2013-05-07
*
Incorporated contribution 3667, which fixes bug in /z3exe flag (http://boogie...
Rustan Leino
2012-11-20
*
Z3: do not assert that the ProgramFiles environment variable is set
Peter Collingbourne
2012-05-02
*
minor fix in tracing
qadeer
2012-02-14
*
minor bug in printing z3 path when running with /trace
qadeer
2012-02-09
*
Boogie: Updated the error message for old versions of Z3.
wuestholz
2011-10-28
*
Boogie: Present a nice error message when Z3 of lesser version than 3.2 is found
Michal Moskal
2011-10-27
*
Don't pass /T: option to Z3 - it kills Z3 prematurely when there are multiple...
Michal Moskal
2011-10-21
*
Add PROVER_PATH prover option (to base options, but currently only used by SM...
Michal Moskal
2011-08-29
*
deleted lazyinlining option 2 and 3
qadeer
2011-08-17
*
Add /T: option to Z3 to kill it if it exceeds soft timeout by more than 1s
Michal Moskal
2011-06-30
*
Use :reason-unknown not :last-failure for Z3 in SMT mode; disable SORT_AND_OR...
Michal Moskal
2011-04-28
*
Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)
MichalMoskal
2011-02-23
*
Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!)
MichalMoskal
2011-02-23
*
Parse else-> clauses in the model
MichalMoskal
2011-02-23
*
Ask Z3 to generate models, in V2 format, when needed
MichalMoskal
2011-02-18
*
Disable MBQI and AUTO_CONFIG
MichalMoskal
2011-02-17
*
Provide /p: as the short form of /proverOpt:.
MichalMoskal
2011-02-17
*
Make it possible to run Z3 on pipe; use generic PROVER_LOG options
MichalMoskal
2011-02-17