Fix SMT test

Leo Alt · ekpyron · commit 937af7d72242 · 2021-08-12T22:34:18.000+02:00
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol
@@ -14,6 +14,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
-// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
+// Warning 6328: (69-85): CHC: Assertion violation happens here.
+// Warning 6328: (177-191): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol
@@ -11,5 +11,7 @@ contract C {
 		assert(a == 2); // should fail
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (253-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nd = 0\na = 3\n\nTransaction trace:\nC.constructor(0)
+// Warning 6328: (253-267): CHC: Assertion violation happens here.

Original file line number	Diff line number	Diff line change
`@@ -11,5 +11,7 @@ contract C {`
`11`	`11`	`assert(a == 2); // should fail`
`12`	`12`	`}`
`13`	`13`	`}`
	`14`	`+// ====`
	`15`	`+// SMTIgnoreCex: yes`
`14`	`16`	`// ----`
`15`		`-// Warning 6328: (253-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nd = 0\na = 3\n\nTransaction trace:\nC.constructor(0)`
	`17`	`+// Warning 6328: (253-267): CHC: Assertion violation happens here.`