index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Boogie build succeeded, 4 test(s) failed
codeplexbot
2011-02-23
*
Boogie build succeeded, 26 test(s) failed
codeplexbot
2011-02-23
*
Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly different...
MichalMoskal
2011-02-23
*
Check for timeout/memoryout
MichalMoskal
2011-02-23
*
Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq thing...
MichalMoskal
2011-02-23
*
Don't try to declare bv types
MichalMoskal
2011-02-23
*
Dispose of the prover when Close() is called.
MichalMoskal
2011-02-23
*
Add workaround for cmd race
MichalMoskal
2011-02-23
*
Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!)
MichalMoskal
2011-02-23
*
Pass solverarguments
MichalMoskal
2011-02-23
*
Do typed->untyped translation for -mv variables
MichalMoskal
2011-02-23
*
Provide dummy implementation of FlushAxiomsToTheoremProver()
MichalMoskal
2011-02-23
*
Handle as-array[...] model elements
MichalMoskal
2011-02-23
*
Fixes in /useArrayTheory handling
MichalMoskal
2011-02-23
*
Parse else-> clauses in the model
MichalMoskal
2011-02-23
*
Throw exceptions when push/pop interface is used but not implemented
MichalMoskal
2011-02-23
*
Pass :skolemid to SMTLib prover
MichalMoskal
2011-02-23
*
Implement Push/Pop interface.
MichalMoskal
2011-02-23
*
Allow recent Z3 versions to be used
MichalMoskal
2011-02-21
*
Move model printing to ErrorModel class
MichalMoskal
2011-02-21
*
Per SMT standard push requires an argument
MichalMoskal
2011-02-21
*
Add some ExpertLevel functions
MichalMoskal
2011-02-21
*
Set Id of Elements.
MichalMoskal
2011-02-21
*
Dafny: Improved scheme for splitting expressions. Also, report each split i...
rustanleino
2011-02-19
*
Print prover errors on stdout (same as prover warnings)
MichalMoskal
2011-02-18
*
Fix help for /mv
MichalMoskal
2011-02-18
*
Don't run test21 with the untyped Z3, as this is no longer going to be available
MichalMoskal
2011-02-18
*
Run dafny and boogie tests by default
MichalMoskal
2011-02-18
*
Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3
MichalMoskal
2011-02-18
*
Accomodate for recent changes in Z3 V2 model format
MichalMoskal
2011-02-18
*
Ask Z3 to generate models, in V2 format, when needed
MichalMoskal
2011-02-18
*
Don't stop when some test fails
MichalMoskal
2011-02-18
*
Handle /useArrayTheory
MichalMoskal
2011-02-18
*
Add tickleBool
MichalMoskal
2011-02-18
*
Allow for running Boogie and Dafny testcases separately
MichalMoskal
2011-02-18
*
Remove a testcase for bvInt (feature to be killed soon)
MichalMoskal
2011-02-18
*
Allow for passing flags to test runs
MichalMoskal
2011-02-18
*
Intercept Z3 warnings and pass them on
MichalMoskal
2011-02-18
*
Boogie build succeeded, 4 test(s) failed
codeplexbot
2011-02-18
*
Remove workaround for Z3 scanner problems (fixed now); fix one comment
MichalMoskal
2011-02-18
*
Recognize () as identifier terminators
MichalMoskal
2011-02-18
*
Handle bitvectors
MichalMoskal
2011-02-18
*
Expose ToByteArray()
MichalMoskal
2011-02-18
*
Dafny:
rustanleino
2011-02-17
*
Boogie: Fixed problem with binding power of .[.] versus type coercions in pre...
rustanleino
2011-02-17
*
Use explicit mechanism for skipping to the next assertion
MichalMoskal
2011-02-17
*
Disable MBQI and AUTO_CONFIG
MichalMoskal
2011-02-17
*
Kill the solver process when ctrl-c is pressed
MichalMoskal
2011-02-17
*
Provide /p: as the short form of /proverOpt:.
MichalMoskal
2011-02-17
*
Read prover responses; handle labels
MichalMoskal
2011-02-17
[prev]
[next]