update test expectations

ethereum · May 9, 2024 · ce2a40e · ce2a40e
1 parent 3c5aa3b
commit ce2a40e
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 9 deletions.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
@@ -19,5 +19,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (280-314): CHC: Assertion violation happens here.
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 1236: (175-190): BMC: Insufficient funds happens here.
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
@@ -16,8 +16,8 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 8656: (141-156): CHC: Insufficient funds happens here.
 // Warning 6328: (193-226): CHC: Assertion violation might happen here.
 // Warning 6328: (245-279): CHC: Assertion violation happens here.
 // Warning 6328: (298-332): CHC: Assertion violation happens here.
-// Warning 1236: (141-156): BMC: Insufficient funds happens here.
 // Warning 4661: (193-226): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol
@@ -18,4 +18,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
@@ -20,5 +20,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (258-274): CHC: Assertion violation happens here.
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 1236: (33-46): BMC: Insufficient funds happens here.
+// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
@@ -23,5 +23,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (315-331): CHC: Assertion violation happens here.
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 1236: (87-100): BMC: Insufficient funds happens here.
+// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol
@@ -21,6 +21,6 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.
+// Warning 8656: (54-67): CHC: Insufficient funds happens here.
 // Warning 6328: (282-298): CHC: Assertion violation happens here.
 // Warning 6328: (317-331): CHC: Assertion violation happens here.
-// Warning 1236: (54-67): BMC: Insufficient funds happens here.