Move CHC counterexamples to primary location

libsolidity/formal/CHC.cpp

@@ -1387,8 +1387,7 @@ void CHC::checkAndReportTarget(
 			m_errorReporter.warning(
 				_errorReporterId,
 				location,
-				"CHC: " + _satMsg,
+				"CHC: " + _satMsg + "\nCounterexample:\n" + *cex
-				SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{})
 			);
 		else
 			m_errorReporter.warning(

test/cmdlineTests/model_checker_engine_all/err

@@ -1,9 +1,5 @@
 Warning: CHC: Assertion violation happens here.
- --> model_checker_engine_all/input.sol:6:3:
+Counterexample:
-  |
-6 | 		assert(x > 0);
-  | 		^^^^^^^^^^^^^
-Note: Counterexample:
 
 x = 0
 
@@ -11,3 +7,7 @@ x = 0
 Transaction trace:
 constructor()
 f(0)
+ --> model_checker_engine_all/input.sol:6:3:
+  |
+6 | 		assert(x > 0);
+  | 		^^^^^^^^^^^^^

test/cmdlineTests/model_checker_engine_chc/err

@@ -1,9 +1,5 @@
 Warning: CHC: Assertion violation happens here.
- --> model_checker_engine_chc/input.sol:6:3:
+Counterexample:
-  |
-6 | 		assert(x > 0);
-  | 		^^^^^^^^^^^^^
-Note: Counterexample:
 
 x = 0
 
@@ -11,3 +7,7 @@ x = 0
 Transaction trace:
 constructor()
 f(0)
+ --> model_checker_engine_chc/input.sol:6:3:
+  |
+6 | 		assert(x > 0);
+  | 		^^^^^^^^^^^^^

test/cmdlineTests/standard_model_checker_engine_all/output.json

@@ -1,6 +1,4 @@
 {"errors":[{"component":"general","errorCode":"6328","formattedMessage":"A:4:47: Warning: CHC: Assertion violation happens here.
-contract C { function f(uint x) public pure { assert(x > 0); } }
-                                              ^-----------^
 Counterexample:
 
 x = 0
@@ -9,11 +7,14 @@ x = 0
 Transaction trace:
 constructor()
 f(0)
-","message":"CHC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
+contract C { function f(uint x) public pure { assert(x > 0); } }
+                                              ^-----------^
+","message":"CHC: Assertion violation happens here.
+Counterexample:
 
 x = 0
 
 
 Transaction trace:
 constructor()
-f(0)"}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}
+f(0)","severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_engine_chc/output.json

@@ -1,6 +1,4 @@
 {"errors":[{"component":"general","errorCode":"6328","formattedMessage":"A:4:47: Warning: CHC: Assertion violation happens here.
-contract C { function f(uint x) public pure { assert(x > 0); } }
-                                              ^-----------^
 Counterexample:
 
 x = 0
@@ -9,11 +7,14 @@ x = 0
 Transaction trace:
 constructor()
 f(0)
-","message":"CHC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
+contract C { function f(uint x) public pure { assert(x > 0); } }
+                                              ^-----------^
+","message":"CHC: Assertion violation happens here.
+Counterexample:
 
 x = 0
 
 
 Transaction trace:
 constructor()
-f(0)"}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}
+f(0)","severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/libsolidity/SMTCheckerTest.cpp

@@ -53,6 +53,14 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
 
 	if (m_enabledSolvers.none() || m_modelCheckerSettings.engine.none())
 		m_shouldRun = false;
+
+	auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "no");
+	if (ignoreCex == "no")
+		m_ignoreCex = false;
+	else if (ignoreCex == "yes")
+		m_ignoreCex = true;
+	else
+		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice."));
 }
 
 TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
@@ -65,3 +73,20 @@ TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePr
 
 	return conclude(_stream, _linePrefix, _formatted);
 }
+
+void SMTCheckerTest::filterObtainedErrors()
+{
+	SyntaxTest::filterObtainedErrors();
+
+	static auto removeCex = [](vector<SyntaxTestError>& errors) {
+		for (auto& e: errors)
+			if (
+				auto cexPos = e.message.find("\\nCounterexample");
+				cexPos != string::npos
+			)
+				e.message = e.message.substr(0, cexPos);
+	};
+
+	if (m_ignoreCex)
+		removeCex(m_errorList);
+}

test/libsolidity/SMTCheckerTest.h

@@ -40,6 +40,8 @@ public:
 
 	TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
 
+	void filterObtainedErrors() override;
+
 protected:
 	/// This contains engine and timeout.
 	/// The engine can be set via option SMTEngine in the test.
@@ -51,6 +53,8 @@ protected:
 	/// The possible options are `all`, `z3`, `cvc4`, `none`,
 	/// where if none is given the default used option is `all`.
 	smtutil::SMTSolverChoice m_enabledSolvers;
+
+	bool m_ignoreCex = false;
 };
 
 }

test/libsolidity/SyntaxTest.h

@@ -52,7 +52,7 @@ public:
 protected:
 	void setupCompiler();
 	void parseAndAnalyze() override;
-	void filterObtainedErrors();
+	virtual void filterObtainedErrors();
 
 	bool m_optimiseYul = true;
 	bool m_parserErrorRecovery = false;

test/libsolidity/smtCheckerTests/array_members/array_pop_length_1.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" happens here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/array_pop_length_2.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" happens here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/array_pop_length_3.sol

@@ -8,5 +8,5 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" happens here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()
-// Warning 2529: (93-100): CHC: Empty array "pop" happens here.
+// Warning 2529: (93-100): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/array_pop_length_4.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (94-101): CHC: Empty array "pop" happens here.
+// Warning 2529: (94-101): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/array_pop_length_5.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (122-129): CHC: Empty array "pop" happens here.
+// Warning 2529: (122-129): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/array_pop_length_6.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (127-134): CHC: Empty array "pop" happens here.
+// Warning 2529: (127-134): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/array_pop_length_8.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" happens here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/length_basic.sol

@@ -10,4 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (153-176): CHC: Assertion violation happens here.
+// Warning 6328: (153-176): CHC: Assertion violation happens here.\nCounterexample:\narr = []\n\n\n\nTransaction trace:\nconstructor()\nState: arr = []\nf()

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol

@@ -14,6 +14,6 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (198-224): CHC: Assertion violation happens here.
+// Warning 6328: (198-224): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\n\n\nTransaction trace:\nconstructor()\nState: arr = [], arr2 = []\nf()
-// Warning 6328: (228-254): CHC: Assertion violation happens here.
+// Warning 6328: (228-254): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\n\n\nTransaction trace:\nconstructor()\nState: arr = [], arr2 = []\nf()
-// Warning 6328: (258-281): CHC: Assertion violation happens here.
+// Warning 6328: (258-281): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\n\n\nTransaction trace:\nconstructor()\nState: arr = [], arr2 = []\nf()

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol

@@ -16,7 +16,7 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (222-248): CHC: Assertion violation happens here.
+// Warning 6328: (222-248): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\n\n\nTransaction trace:\nconstructor()\nState: arr = [], arr2 = []\nf()
-// Warning 6328: (252-278): CHC: Assertion violation happens here.
+// Warning 6328: (252-278): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\n\n\nTransaction trace:\nconstructor()\nState: arr = [], arr2 = []\nf()
-// Warning 6328: (282-305): CHC: Assertion violation happens here.
+// Warning 6328: (282-305): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\n\n\nTransaction trace:\nconstructor()\nState: arr = [], arr2 = []\nf()
-// Warning 6328: (309-335): CHC: Assertion violation happens here.
+// Warning 6328: (309-335): CHC: Assertion violation happens here.\nCounterexample:\narr = [], arr2 = []\n\n\n\nTransaction trace:\nconstructor()\nState: arr = [], arr2 = []\nf()

test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): CHC: Empty array "pop" happens here.
+// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (111-121): CHC: Empty array "pop" happens here.
+// Warning 2529: (111-121): CHC: Empty array "pop" happens here.\nCounterexample:\na = [[0]]\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (76-83): CHC: Empty array "pop" happens here.
+// Warning 2529: (76-83): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\n\n\nTransaction trace:\nconstructor()

test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (150-157): CHC: Empty array "pop" happens here.
+// Warning 2529: (150-157): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\nl = 0\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf(0)

test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol

@@ -9,6 +9,8 @@ contract C {
 		assert(a[0][a[0].length - 1] == y);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 3944: (162-177): CHC: Underflow (resulting value less than 0) happens here.
 // Warning 6328: (150-184): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol

@@ -18,4 +18,4 @@ contract C {
 
 }
 // ----
-// Warning 6328: (232-262): CHC: Assertion violation happens here.
+// Warning 6328: (232-262): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\ng()

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol

@@ -21,4 +21,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (395-453): CHC: Assertion violation happens here.
+// Warning 6328: (395-453): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\n\n\n\nTransaction trace:\nconstructor()\nState: c = []\ng()

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (237-263): CHC: Assertion violation happens here.
+// Warning 6328: (237-263): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\nf()

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_1.sol

@@ -16,4 +16,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (317-343): CHC: Assertion violation happens here.
+// Warning 6328: (317-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [[0], [0]]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\nf()

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol

@@ -8,5 +8,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (113-139): CHC: Assertion violation happens here.
+// Warning 6328: (113-139): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\nl()
-// Warning 6328: (143-189): CHC: Assertion violation happens here.
+// Warning 6328: (143-189): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\nl()

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol

@@ -10,6 +10,6 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (122-148): CHC: Assertion violation happens here.
+// Warning 6328: (122-148): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\n\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\nl()
-// Warning 6328: (202-218): CHC: Assertion violation happens here.
+// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\n\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\nl()
-// Warning 6328: (222-278): CHC: Assertion violation happens here.
+// Warning 6328: (222-278): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\n\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\nl()

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol

@@ -11,6 +11,8 @@ contract C {
 		assert(a[0][a[0].length - 1] == 8);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 3944: (217-232): CHC: Underflow (resulting value less than 0) happens here.
 // Warning 6328: (205-239): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol

@@ -12,4 +12,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (167-188): CHC: Assertion violation happens here.
+// Warning 6328: (167-188): CHC: Assertion violation happens here.\nCounterexample:\na = [[17, 12, 12, 12, 12], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15]]\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (111-144): CHC: Assertion violation happens here.
+// Warning 6328: (111-144): CHC: Assertion violation happens here.\nCounterexample:\na = [[0]]\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (94-124): CHC: Assertion violation happens here.
+// Warning 6328: (94-124): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol

@@ -15,4 +15,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (184-213): CHC: Assertion violation happens here.
+// Warning 6328: (184-213): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [], []]\n\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\nl()

test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol

@@ -10,4 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (199-234): CHC: Assertion violation happens here.
+// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\n\nTransaction trace:\nconstructor()\nf(2437)

test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol

@@ -53,4 +53,4 @@ contract MyConc{
 // ----
 // Warning 2519: (773-792): This declaration shadows an existing declaration.
 // Warning 2018: (1009-1086): Function state mutability can be restricted to view
-// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nA = 1, should_be_constant = 0, should_be_constant_2 = 2, not_constant = 0, not_constant_2 = 115792089237316195423570985008687907853269984665640564039457584007913129639926, not_constant_3 = 0\n\nTransaction trace:\nconstructor()

test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol

@@ -21,4 +21,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (359-373): CHC: Assertion violation happens here.
+// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol

@@ -21,4 +21,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (365-379): CHC: Assertion violation happens here.
+// Warning 6328: (365-379): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol

@@ -21,4 +21,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (358-372): CHC: Assertion violation happens here.
+// Warning 6328: (358-372): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol

@@ -21,4 +21,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (365-379): CHC: Assertion violation happens here.
+// Warning 6328: (365-379): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol

@@ -23,4 +23,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (103-117): CHC: Assertion violation happens here.
+// Warning 6328: (103-117): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ntest()

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol

@@ -42,6 +42,6 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (384-398): CHC: Assertion violation happens here.
+// Warning 6328: (384-398): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ntest()
-// Warning 6328: (635-652): CHC: Assertion violation happens here.
+// Warning 6328: (635-652): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nset(1)\nState: x = 1\ntest()
-// Warning 6328: (781-795): CHC: Assertion violation happens here.
+// Warning 6328: (781-795): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nset(10)\nState: x = 10\ntest()

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init.sol

@@ -35,7 +35,7 @@ contract C is B {
 	}
 }
 // ----
-// Warning 6328: (330-344): CHC: Assertion violation happens here.
+// Warning 6328: (330-344): CHC: Assertion violation happens here.\nCounterexample:\ny = 2, x = (- 1)\na = 1\n\n\nTransaction trace:\nconstructor(1)
-// Warning 6328: (422-445): CHC: Assertion violation happens here.
+// Warning 6328: (422-445): CHC: Assertion violation happens here.\nCounterexample:\ny = 2, x = (- 1)\na = 1\n\n\nTransaction trace:\nconstructor(1)
-// Warning 6328: (522-546): CHC: Assertion violation happens here.
+// Warning 6328: (522-546): CHC: Assertion violation happens here.\nCounterexample:\ny = 4, x = 0\na = 0\n\n\nTransaction trace:\nconstructor(0)
-// Warning 6328: (566-579): CHC: Assertion violation happens here.
+// Warning 6328: (566-579): CHC: Assertion violation happens here.\nCounterexample:\ny = 4, x = 0\na = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol

@@ -25,4 +25,4 @@ contract D is C {
 	}
 }
 // ----
-// Warning 6328: (319-333): CHC: Assertion violation happens here.
+// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\na = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_diamond.sol

@@ -60,11 +60,11 @@ contract D4 is B, C {
 	}
 }
 // ----
-// Warning 6328: (370-384): CHC: Assertion violation happens here.
+// Warning 6328: (370-384): CHC: Assertion violation happens here.\nCounterexample:\nz = 1, y = 1, x = 0\n\n\n\nTransaction trace:\nconstructor()
-// Warning 6328: (403-418): CHC: Assertion violation happens here.
+// Warning 6328: (403-418): CHC: Assertion violation happens here.\nCounterexample:\nz = 1, y = 1, x = 0\n\n\n\nTransaction trace:\nconstructor()
-// Warning 6328: (493-507): CHC: Assertion violation happens here.
+// Warning 6328: (493-507): CHC: Assertion violation happens here.\nCounterexample:\nz = 2, y = 1, x = (- 1)\n\n\n\nTransaction trace:\nconstructor()
-// Warning 6328: (526-540): CHC: Assertion violation happens here.
+// Warning 6328: (526-540): CHC: Assertion violation happens here.\nCounterexample:\nz = 2, y = 1, x = (- 1)\n\n\n\nTransaction trace:\nconstructor()
-// Warning 6328: (703-717): CHC: Assertion violation happens here.
+// Warning 6328: (703-717): CHC: Assertion violation happens here.\nCounterexample:\nz = 1, y = 2, x = 1\n\n\n\nTransaction trace:\nconstructor()
-// Warning 6328: (769-784): CHC: Assertion violation happens here.
+// Warning 6328: (769-784): CHC: Assertion violation happens here.\nCounterexample:\nz = 1, y = 2, x = 1\n\n\n\nTransaction trace:\nconstructor()
-// Warning 6328: (860-874): CHC: Assertion violation happens here.
+// Warning 6328: (860-874): CHC: Assertion violation happens here.\nCounterexample:\nz = 2, y = 2, x = (- 1)\n\n\n\nTransaction trace:\nconstructor()
-// Warning 6328: (893-907): CHC: Assertion violation happens here.
+// Warning 6328: (893-907): CHC: Assertion violation happens here.\nCounterexample:\nz = 2, y = 2, x = (- 1)\n\n\n\nTransaction trace:\nconstructor()

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol

@@ -26,6 +26,6 @@ contract C is B {
 }
 // ----
 // Warning 5740: (152-157): Unreachable code.
-// Warning 6328: (310-324): CHC: Assertion violation happens here.
+// Warning 6328: (310-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 1\n\n\nTransaction trace:\nconstructor(1)
-// Warning 6328: (343-357): CHC: Assertion violation happens here.
+// Warning 6328: (343-357): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 1\n\n\nTransaction trace:\nconstructor(1)
-// Warning 6328: (376-390): CHC: Assertion violation happens here.
+// Warning 6328: (376-390): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/nested_if.sol

@@ -22,5 +22,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (147-174): CHC: Assertion violation happens here.
+// Warning 6328: (147-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 2\n\n\nTransaction trace:\nconstructor()\ntest(0, 2)
 // Warning 6838: (332-348): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if2.sol

@@ -14,4 +14,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (89-114): CHC: Assertion violation happens here.
+// Warning 6328: (89-114): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\n\nTransaction trace:\nconstructor()\ntest(0)

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_array.sol

@@ -25,4 +25,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (205-222): CHC: Assertion violation happens here.
+// Warning 6328: (205-222): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\n\n\nTransaction trace:\nconstructor()\nState: a = [0, 0]\ncheck()

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_state_var.sol

@@ -19,4 +19,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (132-146): CHC: Assertion violation happens here.
+// Warning 6328: (132-146): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ncheck()

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct.sol

@@ -22,4 +22,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (156-172): CHC: Assertion violation happens here.
+// Warning 6328: (156-172): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0}\n\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0}\ncheck()

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct_2.sol

@@ -22,4 +22,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (156-172): CHC: Assertion violation happens here.
+// Warning 6328: (156-172): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0}\n\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0}\ncheck()

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_tuple.sol

@@ -23,5 +23,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (160-174): CHC: Assertion violation happens here.
+// Warning 6328: (160-174): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\ncheck()
-// Warning 6328: (194-208): CHC: Assertion violation happens here.
+// Warning 6328: (194-208): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\ncheck()

test/libsolidity/smtCheckerTests/control_flow/require.sol

@@ -31,4 +31,4 @@ contract C {
 }
 // ----
 // Warning 6321: (429-442): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
-// Warning 6328: (448-465): CHC: Assertion violation happens here.
+// Warning 6328: (448-465): CHC: Assertion violation happens here.\nCounterexample:\nx = true\n\n\n\nTransaction trace:\nconstructor()\nState: x = false\ni()

test/libsolidity/smtCheckerTests/control_flow/return_1_fail.sol

@@ -19,8 +19,8 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (244-270): CHC: Assertion violation happens here.
+// Warning 6328: (244-270): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
-// Warning 6328: (274-300): CHC: Assertion violation happens here.
+// Warning 6328: (274-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
-// Warning 6328: (304-330): CHC: Assertion violation happens here.
+// Warning 6328: (304-330): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
-// Warning 6328: (334-362): CHC: Assertion violation happens here.
+// Warning 6328: (334-362): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
 // Warning 2661: (158-161): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/control_flow/return_2_fail.sol

@@ -27,6 +27,8 @@ contract C {
 		assert(c != 0xffffffff);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (303-329): CHC: Assertion violation happens here.
 // Warning 6328: (333-350): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/revert.sol

@@ -33,4 +33,4 @@ contract C {
 // Warning 5740: (116-129): Unreachable code.
 // Warning 5740: (221-234): Unreachable code.
 // Warning 6321: (408-421): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
-// Warning 6328: (427-444): CHC: Assertion violation happens here.
+// Warning 6328: (427-444): CHC: Assertion violation happens here.\nCounterexample:\nx = true\n\n\n\nTransaction trace:\nconstructor()\nState: x = false\ni()

test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol

@@ -14,5 +14,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (183-197): CHC: Assertion violation happens here.
+// Warning 6328: (183-197): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\na = 0\n\n\nTransaction trace:\nconstructor()\nf(false, 0)
 // Warning 6838: (155-156): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (227-236): CHC: Assertion violation happens here.
+// Warning 6328: (227-236): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n = false\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol

@@ -17,5 +17,5 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (202-218): CHC: Assertion violation happens here.
+// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n\n = false\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()
-// Warning 6328: (242-252): CHC: Assertion violation happens here.
+// Warning 6328: (242-252): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n\n = false\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (225-235): CHC: Assertion violation happens here.
+// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n = false\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (225-235): CHC: Assertion violation happens here.
+// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n = false\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol

@@ -24,4 +24,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (360-370): CHC: Assertion violation happens here.
+// Warning 6328: (360-370): CHC: Assertion violation happens here.\nCounterexample:\nx = 102\na = false\n = false\n\nTransaction trace:\nconstructor()\nState: x = 0\ng(false)

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (225-235): CHC: Assertion violation happens here.
+// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n = false\n\nTransaction trace:\nconstructor()\nState: x = 0\ng()

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (159-173): CHC: Assertion violation happens here.
+// Warning 6328: (159-173): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\n\n\nTransaction trace:\nconstructor()\nf(11)

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (159-173): CHC: Assertion violation happens here.
+// Warning 6328: (159-173): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\n\n\nTransaction trace:\nconstructor()\nf(11)

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (161-175): CHC: Assertion violation happens here.
+// Warning 6328: (161-175): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 11\n\n\nTransaction trace:\nconstructor()\nf(11)

test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol

@@ -11,6 +11,6 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (183-197): CHC: Assertion violation happens here.
+// Warning 6328: (183-197): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7])
-// Warning 6328: (201-215): CHC: Assertion violation happens here.
+// Warning 6328: (201-215): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [9, 9]\n\n\nTransaction trace:\nconstructor()\nf([9, 9])
-// Warning 6328: (219-233): CHC: Assertion violation happens here.
+// Warning 6328: (219-233): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7])

test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol

@@ -29,7 +29,7 @@ contract C {
 // Warning 6328: (305-321): CHC: Assertion violation might happen here.
 // Warning 1218: (448-464): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (448-464): CHC: Assertion violation might happen here.
-// Warning 6328: (673-689): CHC: Assertion violation happens here.
+// Warning 6328: (673-689): CHC: Assertion violation happens here.\nCounterexample:\n\nh0 = 21238\nv0 = 173\nr0 = 30612\ns0 = 32285\nh1 = 7719\nv1 = 21\nr1 = 10450\ns1 = 8855\n\n\nTransaction trace:\nconstructor()\ne(21238, 173, 30612, 32285, 7719, 21, 10450, 8855)
 // Warning 4661: (168-184): BMC: Assertion violation happens here.
 // Warning 4661: (305-321): BMC: Assertion violation happens here.
 // Warning 4661: (448-464): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (229-243): CHC: Assertion violation happens here.
+// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7])

test/libsolidity/smtCheckerTests/external_calls/external.sol

@@ -17,4 +17,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (200-214): CHC: Assertion violation happens here.
+// Warning 6328: (200-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\nf()\nState: x = 1, d = 0\nf()\nState: x = 2, d = 0\ng()

test/libsolidity/smtCheckerTests/external_calls/external_hash.sol

@@ -25,5 +25,7 @@ contract C {
 		assert(sig_1 == sig_2);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (423-445): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol

@@ -27,5 +27,7 @@ contract C {
 		assert(sig_1 == sig_2);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (431-453): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol

@@ -34,4 +34,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (528-565): CHC: Assertion violation happens here.
+// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\ninv()

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -29,4 +29,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (299-313): CHC: Assertion violation happens here.
+// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 0, y = 0, s = 0\nf()

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol

@@ -41,6 +41,8 @@ contract C {
 		return y;
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (452-466): CHC: Assertion violation happens here.
 // Warning 6328: (470-496): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol

@@ -33,6 +33,8 @@ contract C {
 		return y;
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (381-395): CHC: Assertion violation happens here.
 // Warning 6328: (399-425): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol

@@ -38,5 +38,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (435-461): CHC: Assertion violation happens here.
+// Warning 6328: (435-461): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 0, y = 0, z = 0, s = 0\nf()
-// Warning 6328: (594-631): CHC: Assertion violation happens here.
+// Warning 6328: (594-631): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\ninv()

test/libsolidity/smtCheckerTests/external_calls/external_inc.sol

@@ -18,5 +18,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (189-203): CHC: Assertion violation happens here.
+// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\nf()
 // Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol

@@ -27,4 +27,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (307-321): CHC: Assertion violation happens here.
+// Warning 6328: (307-321): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, d = 0, lock = false\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0, lock = false\nf()

test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol

@@ -26,8 +26,8 @@ contract C {
 // ----
 // Warning 6031: (261-267): Internal error: Expression undefined for SMT solver.
 // Warning 7650: (284-296): Assertion checker does not yet support this expression.
-// Warning 6328: (470-495): CHC: Assertion violation happens here.
+// Warning 6328: (470-495): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ncheck()
-// Warning 6328: (540-565): CHC: Assertion violation happens here.
+// Warning 6328: (540-565): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ncheck()
 // Warning 6031: (261-267): Internal error: Expression undefined for SMT solver.
 // Warning 7650: (284-296): Assertion checker does not yet support this expression.
 // Warning 7650: (284-296): Assertion checker does not yet support this expression.

test/libsolidity/smtCheckerTests/function_selector/homer.sol

@@ -43,4 +43,4 @@ contract Homer is ERC165, Simpson {
 
 
 // ----
-// Warning 6328: (1373-1428): CHC: Assertion violation happens here.
+// Warning 6328: (1373-1428): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\ncheck()

test/libsolidity/smtCheckerTests/function_selector/selector_2.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (125-159): CHC: Assertion violation happens here.
+// Warning 6328: (125-159): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()

test/libsolidity/smtCheckerTests/function_selector/selector_3.sol

@@ -11,4 +11,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (175-217): CHC: Assertion violation happens here.
+// Warning 6328: (175-217): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\nf()

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol

@@ -13,4 +13,4 @@ contract A is C {
 	}
 }
 // ----
-// Warning 6328: (152-166): CHC: Assertion violation happens here.
+// Warning 6328: (152-166): CHC: Assertion violation happens here.\nCounterexample:\na = 2\n\n\n\nTransaction trace:\nconstructor()

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol

@@ -4,4 +4,4 @@ contract A is C { constructor() C(2) { assert(a == 2); } }
 contract B is C { constructor() C(3) { assert(a == 3); } }
 contract J is C { constructor() C(3) { assert(a == 4); } }
 // ----
-// Warning 6328: (243-257): CHC: Assertion violation happens here.
+// Warning 6328: (243-257): CHC: Assertion violation happens here.\nCounterexample:\na = 3\n\n\n\nTransaction trace:\nconstructor()

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol

@@ -18,6 +18,8 @@ contract A is B {
 		assert(a == x + 1);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (232-250): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol

@@ -19,5 +19,5 @@ contract A is B {
 }
 // ----
 // Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
-// Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol

@@ -24,6 +24,8 @@ contract A is B2, B1 {
 		assert(a == x + 1);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (314-319): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol

@@ -25,6 +25,6 @@ contract A is B2, B1 {
 	}
 }
 // ----
-// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639934)
 // Warning 4984: (314-319): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 6328: (302-320): CHC: Assertion violation happens here.
+// Warning 6328: (302-320): CHC: Assertion violation happens here.\nCounterexample:\na = 0\nx = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol

@@ -27,7 +27,7 @@ contract A is B2, B1 {
 	}
 }
 // ----
-// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb1 = 0, a = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nx = 1\n\n\nTransaction trace:\nconstructor(1)
-// Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb2 = 0, a = 1\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
-// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb2 = 0, a = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639934)
 // Warning 6328: (334-350): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol

@@ -20,4 +20,4 @@ contract A is B, B2 {
 }
 // ----
 // Warning 5667: (164-170): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (194-208): CHC: Assertion violation happens here.
+// Warning 6328: (194-208): CHC: Assertion violation happens here.\nCounterexample:\na = 2\nx = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol

@@ -19,4 +19,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (194-200): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (224-238): CHC: Assertion violation happens here.
+// Warning 6328: (224-238): CHC: Assertion violation happens here.\nCounterexample:\na = 2\nx = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol

@@ -17,4 +17,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (138-144): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (172-186): CHC: Assertion violation happens here.
+// Warning 6328: (172-186): CHC: Assertion violation happens here.\nCounterexample:\na = 2\nx = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol

@@ -16,4 +16,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (138-144): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (150-164): CHC: Assertion violation happens here.
+// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\na = 2\nx = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol

@@ -27,4 +27,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (254-260): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (284-298): CHC: Assertion violation happens here.
+// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\na = 4\nx = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol

@@ -32,4 +32,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (296-302): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (357-372): CHC: Assertion violation happens here.
+// Warning 6328: (357-372): CHC: Assertion violation happens here.\nCounterexample:\na = 4\nx = 0\n\n\nTransaction trace:\nconstructor(0)

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol

@@ -24,6 +24,8 @@ contract A is B {
 		assert(a == 4);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 4984: (247-252): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (328-342): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol

@@ -23,4 +23,4 @@ contract B is C {
 contract A is B {
 }
 // ----
-// Warning 6328: (266-280): CHC: Assertion violation happens here.
+// Warning 6328: (266-280): CHC: Assertion violation happens here.\nCounterexample:\na = 3\n\n\n\nTransaction trace:\nconstructor()