Merge pull request #15254 from ethereum/smt-test-simplify

SMTChecker: Simplify some of the long running tests

Author: blishko

test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol

@@ -7,9 +7,7 @@ contract C {
 
 		(uint[] memory c, uint[] memory d) = abi.decode(b1, (uint[], uint[]));
 		assert(a.length == c.length);
-		assert(a.length == d.length); // should fail
 		assert(b.length == d.length);
-		assert(b.length == c.length); // should fail
 
 		(uint[] memory e, uint[] memory f, uint[] memory g) = abi.decode(b1, (uint[], uint[], uint[]));
 		assert(e.length == a.length); // should fail
@@ -24,22 +22,18 @@ contract C {
 
 		(uint[] memory k, uint[] memory l) = abi.decode(b2, (uint[], uint[]));
 		assert(k.length == a.length); // should fail
-		assert(k.length == l.length); // should fail
 		assert(l.length == b.length); // should fail
 	}
 }
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (182-210): CHC: Assertion violation happens here.
-// Warning 6328: (335-363): CHC: Assertion violation happens here.
-// Warning 6328: (414-442): CHC: Assertion violation happens here.
-// Warning 6328: (560-588): CHC: Assertion violation happens here.
-// Warning 6328: (607-635): CHC: Assertion violation happens here.
-// Warning 6328: (654-682): CHC: Assertion violation happens here.
-// Warning 6328: (879-916): CHC: Assertion violation happens here.
-// Warning 6328: (1009-1037): CHC: Assertion violation happens here.
-// Warning 6328: (1056-1084): CHC: Assertion violation happens here.
-// Warning 6328: (1103-1131): CHC: Assertion violation happens here.
+// Warning 6328: (182-210): CHC: Assertion violation happens here.\nCounterexample:\n\nc = []\nd = []\ne = []\nf = []\ng = []\nh = []\ni = []\nj = 0\nk = []\nl = []\n\nTransaction trace:\nC.constructor()\nC.abiDecodeArray(b1, b2) -- counterexample incomplete; parameter name used instead of value
+// Warning 6328: (466-494): CHC: Assertion violation happens here.\nCounterexample:\n\nf = [83, 83, 83, 83, 83, 83, 67, 83, 83, 83, 83, 83, 70, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 72, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 71, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83, 83]\ng = [65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 55, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 60, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65]\nh = []\ni = []\nj = 0\nk = []\nl = []\n\nTransaction trace:\nC.constructor()\nC.abiDecodeArray(b1, b2) -- counterexample incomplete; parameter name used instead of value
+// Warning 6328: (513-541): CHC: Assertion violation happens here.\nCounterexample:\n\ng = [65, 65, 65, 65, 65, 65, 65, 64, 65, 47, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 48, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, 65]\nh = []\ni = []\nj = 0\nk = []\nl = []\n\nTransaction trace:\nC.constructor()\nC.abiDecodeArray(b1, b2) -- counterexample incomplete; parameter name used instead of value
+// Warning 6328: (560-588): CHC: Assertion violation happens here.\nCounterexample:\n\nb = []\nd = []\nh = []\ni = []\nj = 0\nk = []\nl = []\n\nTransaction trace:\nC.constructor()\nC.abiDecodeArray(b1, b2) -- counterexample incomplete; parameter name used instead of value
+// Warning 6328: (785-822): CHC: Assertion violation happens here.\nCounterexample:\n\nf = [144]\nj = 8365\nk = []\nl = []\n\nTransaction trace:\nC.constructor()\nC.abiDecodeArray(b1, b2) -- counterexample incomplete; parameter name used instead of value
+// Warning 6328: (915-943): CHC: Assertion violation happens here.\nCounterexample:\n\nj = 8365\nl = [35, 35, 35, 35, 35]\n\nTransaction trace:\nC.constructor()\nC.abiDecodeArray(b1, b2) -- counterexample incomplete; parameter name used instead of value
+// Warning 6328: (962-990): CHC: Assertion violation happens here.\nCounterexample:\n\nj = 32285\n\nTransaction trace:\nC.constructor()\nC.abiDecodeArray(b1, b2) -- counterexample incomplete; parameter name used instead of value
 // Info 1391: CHC: 6 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/array_branch_3d.sol

@@ -15,6 +15,6 @@ contract C
 // ====
 // SMTEngine: chc
 // SMTSolvers: eld
+// SMTTargets: assert
 // ----
-// Warning 6328: (152-174): CHC: Assertion violation happens here.
-// Info 1391: CHC: 9 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Warning 6328: (152-174): CHC: Assertion violation happens here.\nCounterexample:\nc = [[[0]]]\nb = false\n\nTransaction trace:\nC.constructor()\nState: c = [[[0]]]\nC.f(false)

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol

@@ -32,5 +32,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTTargets: assert
 // ----
-// Info 1391: CHC: 29 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 6 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol

@@ -52,5 +52,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTTargets: assert
 // ----
-// Info 1391: CHC: 51 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/type_minmax.sol

@@ -1,12 +1,4 @@
 contract C {
-	function f(uint a) public pure {
-		assert(a <= type(uint).max);
-		assert(a >= type(uint).min);
-		require(a <= type(uint64).max);
-		assert(a <= type(uint64).max);
-		assert(a <= type(uint32).max);
-	}
-
 	function int_min() public pure {
 		int8 int8_min = type(int8).min;
 		assert(int8_min == -2**7);
@@ -81,5 +73,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (178-207): CHC: Assertion violation happens here.
-// Info 1391: CHC: 24 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 21 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/type_simple_range.sol

@@ -0,0 +1,14 @@
+contract C {
+	function f(uint a) public pure {
+		assert(a <= type(uint).max);
+		assert(a >= type(uint).min);
+		require(a <= type(uint64).max);
+		assert(a <= type(uint64).max);
+		assert(a <= type(uint32).max); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (178-207): CHC: Assertion violation happens here.\nCounterexample:\n\na = 4294967296\n\nTransaction trace:\nC.constructor()\nC.f(4294967296)
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.