| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
| |
division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Should not affect function
of other provers. There is an option added in Check.cs to allow creation
of a Checker with a user-specified ProverContext. Also, some extension of
z3api prover context to support conversion of Z3 formulas back to VCExpr.
Finally, some experimental code, not enabled, to allow conversion of loops to
recursion with "head recursion" rather than "tail recursion" (i.e., recursive
call before loop body rather than after).
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
more than one counterexample is needed.
|
| |
|
|
| |
model generation
|
| |
|
|
| |
Also started using the new quantifier api.
|
| | |
|
| | |
|
| | |
|
|
|
Microsoft.Z3.dll and to C#. It does not work yet.
|
Dan Liew
boehmes
Ken McMillan
qadeer