Busy z3 process leaked

[hmijail]

Dafny version

4.7

Code to produce this issue

const C1 : int := 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000
const C2: int := C1 - 1

type T1 = i:nat | i <= 1
type T2 = n:nat | n < 256
type T3 = i:int | 0 <= i <= C2

type T4 = seq<T3> 
type T5 = seq<T1> 
type T6 = seq<T2> 

datatype D = D(
        F1: T4,
        F2: T4,
        F3: T4,
        F4: T5,
        F5: T5,
        F6: T5,
        F7: T5,
        F8: T4,
        F9: T5,
        F10: T4,
        F11: T6)
    {
        predicate wellFormed()
        {
            (0 < |F1| == |F2| == |F3| 
             == |F4| == |F5| 
             == |F6| == |F7| == |F8| == |F9|
             == |F10| == |F11| 
             )
        }
    }

opaque predicate P(t: D)
requires t.wellFormed()
{
    && (forall i:nat | 7<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> (128 * t.F6[i-7] as nat) + (64 * t.F6[i-6] as nat) + (32 * t.F6[i-5] as nat) + (16 * t.F6[i-4] as nat) + (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat == t.F11[i] as nat)
    // $$ assert {:split_here} true;
    && (forall i:nat | 15<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F10[i] as nat == (128 * t.F6[i-15] as nat) + (64 * t.F6[i-14] as nat) + (32 * t.F6[i-13] as nat) + (16 * t.F6[i-12] as nat) + (8 * t.F6[i-11] as nat) + (4 * t.F6[i-10] as nat) + (2 * t.F6[i-9] as nat) + t.F6[i-8] as nat)
    // $$ assert {:split_here} true;
    && (forall i:nat | 3<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F8[i] as nat == (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat)
    && (forall i:nat | 4<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F7[i] == t.F6[i-4])
    && (forall i:nat | 15<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F9[i] == t.F6[i-15])
}

opaque predicate empty(t: D) 
{
    && (1 == |t.F1|
        == |t.F2|
        == |t.F3|
        == |t.F4|
        == |t.F5|
        == |t.F6|
        == |t.F7|
        == |t.F8|
        == |t.F9|
        == |t.F10|
        == |t.F11|)
    && (0 == t.F1[0] as nat
        == t.F2[0] as nat
        == t.F3[0] as nat
        == t.F4[0] as nat
        == t.F5[0] as nat
        == t.F6[0] as nat
        == t.F7[0] as nat
        == t.F8[0] as nat
        == t.F9[0] as nat
        == t.F10[0] as nat
        == t.F11[0] as nat)
}

lemma expensive(t: D) 
    requires empty(t) && t.wellFormed()
{
    reveal empty();
    reveal P();
    assert P(t);
}

lemma cheap(t: D)
    requires empty(t) && t.wellFormed()
{
    reveal empty();

    assert P1(t);
}

 predicate P1(t: D)
requires t.wellFormed()
{
    && P2(t)
    && P3(t)
    && P4(t)
}

 predicate P2(t: D)
requires t.wellFormed()
{
    (forall i:nat | 7<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> (128 * t.F6[i-7] as nat) + (64 * t.F6[i-6] as nat) + (32 * t.F6[i-5] as nat) + (16 * t.F6[i-4] as nat) + (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat == t.F11[i] as nat)

}

 predicate P3(t: D)
requires t.wellFormed()
{ 
    (forall i:nat | 15<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F10[i] as nat == (128 * t.F6[i-15] as nat) + (64 * t.F6[i-14] as nat) + (32 * t.F6[i-13] as nat) + (16 * t.F6[i-12] as nat) + (8 * t.F6[i-11] as nat) + (4 * t.F6[i-10] as nat) + (2 * t.F6[i-9] as nat) + t.F6[i-8] as nat)
}

 predicate P4(t: D)
requires t.wellFormed()
{ 
    && (forall i:nat | 3<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F8[i] as nat == (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat)
    && (forall i:nat | 4<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F7[i] == t.F6[i-4])
    && (forall i:nat | 15<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F9[i] == t.F6[i-15])
}

Command to run and resulting output

$ dafny verify example.dfy --resource-limit 50000000 --filter-symbol cheap --isolate-assertions
bin_issue.wproof.HM.masked.dfy(91,8): Error: Verification out of resource (cheap)
   |
91 |    assert P1(t);
   |         ^^^^^

bin_issue.wproof.HM.masked.dfy(98,7): Related location: this proposition could not be proved
   |
98 |     && P2(t)
   |        ^^^^^

bin_issue.wproof.HM.masked.dfy(107,5): Related location: this proposition could not be proved
    |
107 |     (forall i:nat | 7<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> (128 * t.F6[i-7] as nat) + (64 * t.F6[i-6] as nat) + (32 * t.F6[i-5] as nat) + (16 * t.F6[i-4] as nat) + (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat == t.F11[i] as nat)
    |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Dafny program verifier finished with 16 verified, 0 errors, 1 out of resource

What happened?

Dafny finishes execution as expected.

However, one z3 process keeps running for a while with high CPU load. This is probably a z3 bug (reported here); but still, I wonder if it's something that Dafny should notice or guard against? It looks like currently it doesn't, and the leaked, CPU-consuming z3 process makes next dafny executions look unexplainably slow/resource-heavy, in a way that it's impossible to understand for the unsuspecting user.

(For example, for a good while I thought that those leaked z3 processes were actually in use by VSCode's Dafny server).

(Additionally: if z3 outputs an answer but keeps running, does that mean that the output was actually somehow unfinished? Should dafny react to that?)

What type of operating system are you experiencing the problem on?

Mac

[hmijail]

The z3 issue seems to not be considered a bug. Some changes were seemingly made, but the new version still keeps running for a long time at high CPU usage even if seemingly it's only cleaning-up.

I asked if I can just kill z3 at that point, but got no answer.

I have written my own dafny wrapper that detects leaked z3 after dafny exits, and kills them. However, that only works on the last iteration of dafny measure-complexity. I have seen non-last iterations running for strangely long times, longer than the resource limit would suggest; is it possible that in those cases dafny is waiting for z3 to die, making the verification unnecessarily slow / resource-heavy?

Another possibility is that dafny doesn't wait, but still a leaked z3 in iteration N makes iteration N+{1,2,...} much slower.