Limited number of assignments?

Jun 22, 2011 at 3:57 PM

Hi,

Dafny 2.0.0.0 erroneously reports an assertion violation for the following code. Commenting any assignment (except for b0 of course) solves the problem. Is there something wrong with this code or is there some kind of limitation on the number of variables or assignments allowed in dafny programs ?

Thanks,

  Olivier

 

class assignments {

  var b0 : bool;
  var b1 : bool;
  var b2 : bool;
  var b3 : bool;
  var b4 : bool;
  var b5 : bool;
  var b6 : bool;
  var b7 : bool;
  var b8 : bool;
  var b9 : bool;
  var b10 : bool;
  var b11 : bool;
  var b12 : bool;
  var b13 : bool;
  var b14 : bool;
  var b15 : bool;
  var b16 : bool;
  var b17 : bool;
  var b18 : bool;
  var b19 : bool;
  var b20 : bool;
  var b21 : bool;
  var b22 : bool;
  var b23 : bool;
  var b24 : bool;
  var b25 : bool;
  var b26 : bool;
  var b27 : bool;
  var b28 : bool;
  var b29 : bool;
  var b30 : bool;
  var b31 : bool;
  var b32 : bool;
  var b33 : bool;
  var b34 : bool;
  var b35 : bool;
  var b36 : bool;
  var b37 : bool;
  var b38 : bool;
  var b39 : bool;
  var b40 : bool;
  var b41 : bool;
  var b42 : bool;
  var b43 : bool;
  var b44 : bool;
  var b45 : bool;
  var b46 : bool;
  var b47 : bool;
  var b48 : bool;
  var b49 : bool;
  var b50 : bool;
  var b51 : bool;
  var b52 : bool;
  var b53 : bool;
  var b54 : bool;
  var b55 : bool;
  var b56 : bool;
  var b57 : bool;
  var b58 : bool;
  var b59 : bool;
  var b60 : bool;
  var b61 : bool;
  var b62 : bool;
  var b63 : bool;
  var b64 : bool;
  var b65 : bool;
  var b66 : bool;
  var b67 : bool;
  var b68 : bool;
  var b69 : bool;
  var b70 : bool;
  var b71 : bool;
  var b72 : bool;
  var b73 : bool;
  var b74 : bool;
  var b75 : bool;
  var b76 : bool;
  var b77 : bool;
  var b78 : bool;
  var b79 : bool;
  var b80 : bool;
  var b81 : bool;
  var b82 : bool;
  var b83 : bool;
  var b84 : bool;
  var b85 : bool;
  var b86 : bool;
  var b87 : bool;
  var b88 : bool;
  var b89 : bool;
  var b90 : bool;
  var b91 : bool;
  var b92 : bool;
  var b93 : bool;
  var b94 : bool;
  var b95 : bool;
  var b96 : bool;
  var b97 : bool;
  var b98 : bool;
  var b99 : bool;
  var b100 : bool;
  var b101 : bool;

  method m() 
    modifies {this};
 {
    b0 := false;
    b1 := false;
    b2 := false;
    b3 := false;
    b4 := false;
    b5 := false;
    b6 := false;
    b7 := false;
    b8 := false;
    b9 := false;
    b10 := false;
    b11 := false;
    b12 := false;
    b13 := false;
    b14 := false;
    b15 := false;
    b16 := false;
    b17 := false;
    b18 := false;
    b19 := false;
    b20 := false;
    b21 := false;
    b22 := false;
    b23 := false;
    b24 := false;
    b25 := false;
    b26 := false;
    b27 := false;
    b28 := false;
    b29 := false;
    b30 := false;
    b31 := false;
    b32 := false;
    b33 := false;
    b34 := false;
    b35 := false;
    b36 := false;
    b37 := false;
    b38 := false;
    b39 := false;
    b40 := false;
    b41 := false;
    b42 := false;
    b43 := false;
    b44 := false;
    b45 := false;
    b46 := false;
    b47 := false;
    b48 := false;
    b49 := false;
    b50 := false;
    b51 := false;
    b52 := false;
    b53 := false;
    b54 := false;
    b55 := false;
    b56 := false;
    b57 := false;
    b58 := false;
    b59 := false;
    b60 := false;
    b61 := false;
    b62 := false;
    b63 := false;
    b64 := false;
    b65 := false;
    b66 := false;
    b67 := false;
    b68 := false;
    b69 := false;
    b70 := false;
    b71 := false;
    b72 := false;
    b73 := false;
    b74 := false;
    b75 := false;
    b76 := false;
    b77 := false;
    b78 := false;
    b79 := false;
    b80 := false;
    b81 := false;
    b82 := false;
    b83 := false;
    b84 := false;
    b85 := false;
    b86 := false;
    b87 := false;
    b88 := false;
    b89 := false;
    b90 := false;
    b91 := false;
    b92 := false;
    b93 := false;
    b94 := false;
    b95 := false;
    b96 := false;
    b97 := false;
    b98 := false;
    b99 := false;
    b100 := false;
    b101 := false;

    assert b0==false;
  }

}

 

Coordinator
Jun 30, 2011 at 11:10 PM

Thanks for the bug report.  Boogie used an implicit limit in Z3, which I have now removed for the axioms needed for this (and similar) examples.  The fix is available in Change Set b2e842035186.