| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
| |
preparation for integrating my ported copies of that project. <\Isabelle> <\Boogie>
|
| |
|
|
| |
/stratifiedInline:1.
|
| |
|
|
|
|
|
|
|
| |
* Set Z3's QI_COST as the sum of "weight" and "generation", not their product. This worked better when setting the :weight of a quantifier (see below).
Dafny:
* Improved axiomatization of sequences; in particular, use an axiom to generate terms that say what the two pieces of a concatenation are
* Two of the (previous) sequence axioms could cause a matching loop, in cases where Z3's arithmetic reasoning does not infer all rational arithmetic equalities during instantiation. The effect of this was apparently not noticed before, perhaps the concatenation/drop properties previously had to be supplied in manual assert statements. But now, with the improved sequence axiomatization (see previous bullet), this effect became remarkably noticeable. To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results.
* Removed several assert lemmas that are no longer needed in Test programs (the test programs now contain only about a handful of such lemmas)
|
| | |
|
| |
|
|
|
|
|
|
|
| |
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
|
| |
|
|
| |
slightly more robust.
|
| |
|
|
| |
option is activated by /lazyInline:2. The original method is activated by /lazyInline:1.
|
| | |
|
| |
|
|
|
|
| |
variable analysis as well
2. Separeted model printing from the lazy inlining option
|
| |
|
|
|
| |
2. Added code for printing array partitions
3. Set UseAbstractInterpretation=false in case lazy inlining is being used
|
| |
|
|
| |
functions in TypeDeclCollector.
|
| |
|
|
| |
/lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.
|
| | |
|
| |
|
|
|
|
|
| |
linear procedure call
2. Inlining requires two fields OriginalBlocks and OriginalLocVars in Implementation. These are set just before inlining is called and now I reset them to null afterwards to help garbage collection.
3. Clear live variables right after passification again to help garbage collection.
|
| |
|
|
| |
by explorer
|
| | |
|
| |
|
|
| |
result types of maps are declared before the type of the map itself.
|
| |
|
|
| |
used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.
|
| | |
|
| | |
|
| |
|
|
|
| |
print _all_ the attributes of an assert this time
add simpletypes to the visitor
|
| | |
|
| |
|
|
|
|
| |
is being executed from, then look in "c:\Program Files\Microsoft Research\Z3-2.x\bin" for x := 5,4,3,2,1,0.
This fixes Issue Tracker item 5446.
|
| |
|
|
| |
quantifier. This makes sure that we get the proper DEFTYPEs for bit vector variables, even when they are not used in operator expressions. Fixes issue #5741.
|
| |
|
|
| |
to Z3. By default, both LET TERM and LET FORMULA expressions are used. Mode /z3lets:2 uses only LET FORMULA, which works around a current Z3 issue with LET expressions and nested quantifiers.
|
| | |
|
| |
|
|
| |
Deleted/ignored some binaries in the Binaries directory.
|
| |
|
|
| |
assert (switches off z3's /@ flag).
|
| |
|
|
| |
stdout/stderr
|
| | |
|
| | |
|
| |
|
tabarbe