Use Boogie v2.8.26 (#1092)

This fixes model generation

Author: RustanLeino

Source/Directory.Build.props

@@ -7,7 +7,7 @@
 
   <!-- Boogie dependency -->
   <ItemGroup>
-    <PackageReference Include="Boogie.ExecutionEngine" Version="2.8.21" />
+    <PackageReference Include="Boogie.ExecutionEngine" Version="2.8.26" />
   </ItemGroup>
 
 </Project>

Test/server/counterexample.transcript

@@ -1,6 +1,5 @@
 # RUN: %server "%s" > "%t"
 # RUN: %diff "%s.expect" "%t"
-# XFAIL: *
 
 counterexample
 eyJhcmdzIjpbXSwiZmlsZW5hbWUiOiJjOlxcREVWXFxEYWZueVxcYWJzLmRmeSIsInNvdXJjZSI6Im1ldGhvZCBBYnMoeDogaW50KSBcclxuICAgIHJldHVybnMgKHk6IGludClcclxuZW5zdXJlcyB5ID49IDAge1xyXG4gICAgcmV0dXJuIHg7XHJcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==

Test/server/counterexample.transcript.expect

@@ -6,6 +6,6 @@ c:\DEV\Dafny\abs.dfy(4,4): Error: A postcondition might not hold on this return
 c:\DEV\Dafny\abs.dfy(3,10): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"<initial>","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"(**y#0)","Name":"y","RealName":null,"Value":"(**y#0)"}]},{"Column":15,"Line":3,"Name":"c:\\DEV\\Dafny\\abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"(**y#0)","Name":"y","RealName":null,"Value":"(**y#0)"}]},{"Column":12,"Line":4,"Name":"c:\\DEV\\Dafny\\abs.dfy(4,12)","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"((- 1))'1","Name":"y","RealName":null,"Value":"((- 1))'1"}]}]} COUNTEREXAMPLE_END
+COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"<initial>","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"}]},{"Column":15,"Line":3,"Name":"c:\\DEV\\Dafny\\abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"}]},{"Column":12,"Line":4,"Name":"c:\\DEV\\Dafny\\abs.dfy(4,12)","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"((- 1))'1","Name":"y","RealName":null,"Value":"((- 1))'1"}]}]} COUNTEREXAMPLE_END
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]

Test/server/git-issue223.transcript

@@ -1,6 +1,5 @@
 # RUN: %server "%s" > "%t"
 # RUN: %diff "%s.expect" "%t"
-# XFAIL: *
 
 counterexample
 eyJhcmdzIjpbXSwiZmlsZW5hbWUiOiJjOlxcREVWXFxEYWZueVxcYWJzLmRmeSIsInNvdXJjZSI6Im1ldGhvZCBBYnMoeDogaW50KSBcclxuICAgIHJldHVybnMgKHk6IGludClcclxuZW5zdXJlcyB5ID49IDAge1xyXG4gICAgcmV0dXJuIHg7XHJcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==

Test/server/git-issue223.transcript.expect

@@ -6,7 +6,7 @@ c:\DEV\Dafny\abs.dfy(4,4): Error: A postcondition might not hold on this return
 c:\DEV\Dafny\abs.dfy(3,10): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"<initial>","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"(**y#0)","Name":"y","RealName":null,"Value":"(**y#0)"}]},{"Column":15,"Line":3,"Name":"c:\\DEV\\Dafny\\abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"(**y#0)","Name":"y","RealName":null,"Value":"(**y#0)"}]},{"Column":12,"Line":4,"Name":"c:\\DEV\\Dafny\\abs.dfy(4,12)","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"((- 1))'1","Name":"y","RealName":null,"Value":"((- 1))'1"}]}]} COUNTEREXAMPLE_END
+COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"<initial>","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"}]},{"Column":15,"Line":3,"Name":"c:\\DEV\\Dafny\\abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"}]},{"Column":12,"Line":4,"Name":"c:\\DEV\\Dafny\\abs.dfy(4,12)","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"((- 1))'1","Name":"y","RealName":null,"Value":"((- 1))'1"}]}]} COUNTEREXAMPLE_END
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 
@@ -17,6 +17,6 @@ c:\DEV\Dafny\abs.dfy(4,4): Error: A postcondition might not hold on this return
 c:\DEV\Dafny\abs.dfy(3,10): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"<initial>","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"(**y#0)","Name":"y","RealName":null,"Value":"(**y#0)"}]},{"Column":15,"Line":3,"Name":"c:\\DEV\\Dafny\\abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"(**y#0)","Name":"y","RealName":null,"Value":"(**y#0)"}]},{"Column":12,"Line":4,"Name":"c:\\DEV\\Dafny\\abs.dfy(4,12)","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"((- 1))'1","Name":"y","RealName":null,"Value":"((- 1))'1"}]}]} COUNTEREXAMPLE_END
+COUNTEREXAMPLE_START {"States":[{"Column":0,"Line":0,"Name":"<initial>","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"}]},{"Column":15,"Line":3,"Name":"c:\\DEV\\Dafny\\abs.dfy(3,15): initial state","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"}]},{"Column":12,"Line":4,"Name":"c:\\DEV\\Dafny\\abs.dfy(4,12)","Variables":[{"CanonicalName":"((- 1))","Name":"x","RealName":null,"Value":"((- 1))"},{"CanonicalName":"((- 1))'1","Name":"y","RealName":null,"Value":"((- 1))'1"}]}]} COUNTEREXAMPLE_END
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]