Pass

utwente-fmt · Oct 12, 2023 · 0d8df1e · 0d8df1e
1 parent 9867f86
commit 0d8df1e
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/examples/concepts/javabip/casinoAdjusted/Operator.java b/examples/concepts/javabip/casinoAdjusted/Operator.java
@@ -23,9 +23,10 @@ public class Operator {
     int amountToMove;
 
     //@ requires id != null;
+    //@ requires funds >= 0;
     Operator (Integer id, int funds) throws Exception {
         this.id = id;
-        if (funds < 0) throw new Exception("Cannot have negative funds");
+        // if (funds < 0) throw new Exception("Cannot have negative funds");
         wallet = funds;
         amountToMove = 0;
         //@ ghost System.staticInvariant();

diff --git a/examples/concepts/javabip/casinoBroken/Operator.java b/examples/concepts/javabip/casinoBroken/Operator.java
@@ -23,9 +23,10 @@ public class Operator {
     int amountToMove;
 
     //@ requires id != null;
+    //@ requires funds >= 0;
     Operator (Integer id, int funds) throws Exception {
         this.id = id;
-        if (funds < 0) throw new Exception("Cannot have negative funds");
+        // if (funds < 0) throw new Exception("Cannot have negative funds");
         wallet = funds;
         amountToMove = 0;
         //@ ghost System.staticInvariant();

diff --git a/src/rewrite/vct/rewrite/bip/EncodeBip.scala b/src/rewrite/vct/rewrite/bip/EncodeBip.scala
@@ -323,7 +323,7 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) extends Re
             },
             contract(requires = UnitAccountedPredicate(dispatch(constructor.requires)),
               blame = constructor.blame)
-          )(PanicBlame("Unexpected error, failing precondition on JavaBIP constructor should not happen"))
+          )(PanicBlame("Unexpected error, failing precondition on JavaBIP constructor should not happen"))(constructor.o)
         )
       }