Boogie:

* 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)

7 files changed, 2 insertions, 9 deletions

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 19f54d94..bb88b265 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -94,7 +94,6 @@ class Benchmark3 {
       call r.Enqueue(m);

       pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]];

     }

-    assert (forall i :: 0 <= i && i < |perm| ==> perm[i] == pperm[i]); //lemma needed to trigger axiom

   }

   

   

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index fdb23379..80d6b8d6 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -105,9 +105,7 @@ class Map<Key,Value> {
     call p, n, prev := FindIndex(key);

     if (p != null) {

       Keys := Keys[..n] + Keys[n+1..];

-      assert Keys[..n] == old(Keys)[..n] && Keys[n..] == old(Keys)[n+1..];

       Values := Values[..n] + Values[n+1..];

-      assert Values[..n] == old(Values)[..n] && Values[n..] == old(Values)[n+1..];

       nodes := nodes[..n] + nodes[n+1..];

       if (prev == null) {

         head := head.next;

diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy
index 62636ce5..f672950b 100644
--- a/Test/dafny1/ListContents.dfy
+++ b/Test/dafny1/ListContents.dfy
@@ -78,10 +78,8 @@ class Node<T> {
       decreases if current != null then |current.list| else -1;

     {

       var nx := current.next;

-      assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma

 

       // ..., reverse, current, nx, ...

-      assert current.data == current.list[0]; // lemma

       current.next := reverse;

       current.footprint := {current} + reverse.footprint;

       current.list := [current.data] + reverse.list;

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 3e64a4bd..52db9dca 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -67,7 +67,6 @@ class Main {
       {

         var c := root.children[i];

         if (c != null) {

-          ghost var D := S - stackNodes;  assert root in D;

           call RecursiveMarkWorker(c, S, stackNodes + {root});

         }

         i := i + 1;

diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
index ca5f206b..87e63e2c 100644
--- a/Test/vacid0/Composite.dfy
+++ b/Test/vacid0/Composite.dfy
@@ -91,7 +91,6 @@ class Composite {
     var p := parent;

     parent := null;

     if (p != null) {

-      assert (p.left == this) != (p.right == this);

       if (p.left == this) {

         p.left := null;

       } else {

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index 6ae00e24..c5a032fe 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -89,7 +89,7 @@ class LazyInitArray<T> {
   {

     if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

     } else {

-      assert n <= e[i];

+      assert n <= e[i];  // lemma

       b[i] := n;

       c[n] := i;

       ghost var t := d[n];

diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy
index 0e6aff05..2c217264 100644
--- a/Test/vacid0/SparseArray.dfy
+++ b/Test/vacid0/SparseArray.dfy
@@ -87,7 +87,7 @@ class SparseArray<T> {
   {

     if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

     } else {

-      assert n <= e[i];

+      assert n <= e[i];  // lemma

       b := b[i := n];

       c := c[n := i];

       ghost var t := d[n];