Dafny-v3.2 report internal errors on dfy files verifiable with Dafny-v2.3 (650a6bbe)

[superymk]

I wrote dafny files (https://github.com/superymk/iosep_proof/blob/master/proof.zip) which can be successfully verified with Dafny-v2.3 (650a6bb). Now I re-run the proof with the released version of Dafny-v3.2, but got internal errors never happen before.

The command I use for verification is: E:/utils/dafny-v3.2/Dafny.exe /trace /stats /compile:0 /timeLimit:4000 /compile:0 Lemmas_Ops_SubjObjActivate.dfy

The error output is:

Coalescing blocks...
Inlining...

Running abstract interpretation...
  [0.0824425 s]
[TRACE] Using prover: E:\utils\dafny-v3.2\z3\bin\z3.exe
Prover error: Unexpected prover response (getting info about 'unknown' response): (:reason-unknown "Overflow encountered when expanding old_vector")


Verifying CheckWellformed$$_module.__default.Lemma__NewDM__SubjObjActivate__FulfillSI2 ...
  [134.752 s, 56 proof obligations]  inconclusive
C:\Users\Superymk\Desktop\New folder (3)\DetailedModel\Lemmas_Ops_SubjObjActivate.dfy(8,6): Verification inconclusive (CheckWellformed$$_module.__default.Lemma__NewDM__SubjObjActivate__FulfillSI2)

Verifying Impl$$_module.__default.Lemma__NewDM__SubjObjActivate__FulfillSI2 ...
  [1.648 s, 206 proof obligations]  inconclusive
C:\Users\Superymk\Desktop\New folder (3)\DetailedModel\Lemmas_Ops_SubjObjActivate.dfy(8,6): Verification inconclusive (Impl$$_module.__default.Lemma__NewDM__SubjObjActivate__FulfillSI2)
Prover error: Invalid PING response from the prover: unsat


Verifying CheckWellformed$$_module.__default.Lemma__DM__DevActivate__ProveCheckOfDevActivateInK ...
  [11.305 s, 2 proof obligations]  inconclusive
C:\Users\Superymk\Desktop\New folder (3)\DetailedModel\Lemmas_Ops_SubjObjActivate.dfy(61,6): Verification inconclusive (CheckWellformed$$_module.__default.Lemma__DM__DevActivate__ProveCheckOfDevActivateInK)
Prover error: Invalid PING response from the prover: unsat


Verifying Impl$$_module.__default.Lemma__DM__DevActivate__ProveCheckOfDevActivateInK ...
  [1.065 s, 8 proof obligations]  inconclusive
C:\Users\Superymk\Desktop\New folder (3)\DetailedModel\Lemmas_Ops_SubjObjActivate.dfy(61,6): Verification inconclusive (Impl$$_module.__default.Lemma__DM__DevActivate__ProveCheckOfDevActivateInK)
Prover error: Invalid PING response from the prover: unsat


Verifying CheckWellformed$$_module.__default.Lemma__NewDM__DevActivate__OtherDevsHaveUnchangedPIDs ...
  [1.072 s, 18 proof obligations]  inconclusive
C:\Users\Superymk\Desktop\New folder (3)\DetailedModel\Lemmas_Ops_SubjObjActivate.dfy(77,6): Verification inconclusive (CheckWellformed$$_module.__default.Lemma__NewDM__DevActivate__OtherDevsHaveUnchangedPIDs)
Prover error: Invalid PING response from the prover: unsat


Verifying Impl$$_module.__default.Lemma__NewDM__DevActivate__OtherDevsHaveUnchangedPIDs ...
  [1.171 s, 5 proof obligations]  inconclusive
C:\Users\Superymk\Desktop\New folder (3)\DetailedModel\Lemmas_Ops_SubjObjActivate.dfy(77,6): Verification inconclusive (Impl$$_module.__default.Lemma__NewDM__DevActivate__OtherDevsHaveUnchangedPIDs)
Prover error: Invalid PING response from the prover: unsat

...

My PC has 128GB memory and the memory usage is always <= 10% when verifying this file.
With Dafny-v2.3, I can verify each function in <300s. And the verification of the entire file takes <30GB memory.

Thanks!

[keyboardDrummer]

What version of Z3 are you using? E:\utils\dafny-v3.2\z3\bin\z3.exe --version

[superymk]

Z3 version 4.8.5 - 64 bit

[robin-aws]

This is a known Z3 bug that was fixed in more recent versions, which unfortunately Dafny can't easily pick up without huge verification behaviour changes: Z3Prover/z3#2201

When I've encountered it myself, I've usually been able to work around it by reducing the cost of the verification that is hitting it (and features like /vcsSplitOnEveryAssert can be very helpful in narrowing that down). My theory is the bug is tickled by verification that needs a lot of resources, although I haven't dug deeply enough to confirm that.