Merge pull request #9352 from ethereum/smt_cex

[SMTChecker] CHC counterexamples

libsmtutil/CHCSmtLib2Interface.cpp

@@ -83,7 +83,7 @@ void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& _n
 	);
 }
 
-pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(Expression const& _block)
+pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
 {
 	string accumulated{};
 	swap(m_accumulatedOutput, accumulated);
@@ -108,7 +108,7 @@ pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(Expression const& _
 		result = CheckResult::ERROR;
 
 	// TODO collect invariants or counterexamples.
-	return make_pair(result, vector<string>{});
+	return {result, {}};
 }
 
 void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)

libsmtutil/CHCSmtLib2Interface.h

@@ -43,7 +43,7 @@ public:
 
 	void addRule(Expression const& _expr, std::string const& _name) override;
 
-	std::pair<CheckResult, std::vector<std::string>> query(Expression const& _expr) override;
+	std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
 
 	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
 

libsmtutil/CHCSolverInterface.h

@@ -24,6 +24,9 @@
 
 #include <libsmtutil/SolverInterface.h>
 
+#include <map>
+#include <vector>
+
 namespace solidity::smtutil
 {
 
@@ -41,9 +44,18 @@ public:
 	/// Needs to bound all vars as universally quantified.
 	virtual void addRule(Expression const& _expr, std::string const& _name) = 0;
 
-	/// Takes a function application and checks
-	/// for reachability.
-	virtual std::pair<CheckResult, std::vector<std::string>> query(
+	/// first: predicate name
+	/// second: predicate arguments
+	using CexNode = std::pair<std::string, std::vector<std::string>>;
+	struct CexGraph
+	{
+		std::map<unsigned, CexNode> nodes;
+		std::map<unsigned, std::vector<unsigned>> edges;
+	};
+
+	/// Takes a function application _expr and checks for reachability.
+	/// @returns solving result and a counterexample graph, if possible.
+	virtual std::pair<CheckResult, CexGraph> query(
 		Expression const& _expr
 	) = 0;
 };

libsmtutil/Z3CHCInterface.cpp

@@ -20,6 +20,9 @@
 
 #include <libsolutil/CommonIO.h>
 
+#include <set>
+#include <stack>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::smtutil;
@@ -33,17 +36,7 @@ Z3CHCInterface::Z3CHCInterface():
 	z3::set_param("rewriter.pull_cheap_ite", true);
 	z3::set_param("rlimit", Z3Interface::resourceLimit);
 
-	// Spacer options.
-	// These needs to be set in the solver.
-	// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
-	z3::params p(*m_context);
-	// These are useful for solving problems with arrays and loops.
-	// Use quantified lemma generalizer.
-	p.set("fp.spacer.q3.use_qgen", true);
-	p.set("fp.spacer.mbqi", false);
-	// Ground pobs by using values from a model.
-	p.set("fp.spacer.ground_pobs", false);
-	m_solver.set(p);
+	setSpacerOptions();
 }
 
 void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
@@ -72,10 +65,10 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
 	}
 }
 
-pair<CheckResult, vector<string>> Z3CHCInterface::query(Expression const& _expr)
+pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
 {
 	CheckResult result;
-	vector<string> values;
+	CHCSolverInterface::CexGraph cex;
 	try
 	{
 		z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
@@ -84,8 +77,9 @@ pair<CheckResult, vector<string>> Z3CHCInterface::query(Expression const& _expr)
 		case z3::check_result::sat:
 		{
 			result = CheckResult::SATISFIABLE;
-			// TODO retrieve model.
-			break;
+			auto proof = m_solver.get_answer();
+			auto cex = cexGraph(proof);
+			return {result, cex};
 		}
 		case z3::check_result::unsat:
 		{
@@ -104,8 +98,119 @@ pair<CheckResult, vector<string>> Z3CHCInterface::query(Expression const& _expr)
 	catch (z3::exception const&)
 	{
 		result = CheckResult::ERROR;
-		values.clear();
+		cex = {};
 	}
 
-	return make_pair(result, values);
+	return {result, cex};
+}
+
+void Z3CHCInterface::setSpacerOptions(bool _preProcessing)
+{
+	// Spacer options.
+	// These needs to be set in the solver.
+	// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
+	z3::params p(*m_context);
+	// These are useful for solving problems with arrays and loops.
+	// Use quantified lemma generalizer.
+	p.set("fp.spacer.q3.use_qgen", true);
+	p.set("fp.spacer.mbqi", false);
+	// Ground pobs by using values from a model.
+	p.set("fp.spacer.ground_pobs", false);
+
+	// Spacer optimization should be
+	// - enabled for better solving (default)
+	// - disable for counterexample generation
+	p.set("fp.xform.slice", _preProcessing);
+	p.set("fp.xform.inline_linear", _preProcessing);
+	p.set("fp.xform.inline_eager", _preProcessing);
+
+	m_solver.set(p);
+}
+
+/**
+Convert a ground refutation into a linear or nonlinear counterexample.
+The counterexample is given as an implication graph of the form
+`premises => conclusion` where `premises` are the predicates
+from the body of nonlinear clauses, representing the proof graph.
+
+This function is based on and similar to
+https://github.com/Z3Prover/z3/blob/z3-4.8.8/src/muz/spacer/spacer_context.cpp#L2919
+(spacer::context::get_ground_sat_answer)
+which generates linear counterexamples.
+It is modified here to accept nonlinear CHCs as well, generating a DAG
+instead of a path.
+*/
+CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof)
+{
+	CexGraph graph;
+
+	/// The root fact of the refutation proof is `false`.
+	/// The node itself is not a hyper resolution, so we need to
+	/// extract the `query` hyper resolution node from the
+	/// `false` node (the first child).
+	smtAssert(_proof.is_app(), "");
+	smtAssert(fact(_proof).decl().decl_kind() == Z3_OP_FALSE, "");
+
+	stack<z3::expr> proofStack;
+	proofStack.push(_proof.arg(0));
+
+	auto const& root = proofStack.top();
+	graph.nodes[root.id()] = {name(fact(root)), arguments(fact(root))};
+
+	set<unsigned> visited;
+	visited.insert(root.id());
+
+	while (!proofStack.empty())
+	{
+		z3::expr proofNode = proofStack.top();
+		smtAssert(graph.nodes.count(proofNode.id()), "");
+		proofStack.pop();
+
+		if (proofNode.is_app() && proofNode.decl().decl_kind() == Z3_OP_PR_HYPER_RESOLVE)
+		{
+			smtAssert(proofNode.num_args() > 0, "");
+			for (unsigned i = 1; i < proofNode.num_args() - 1; ++i)
+			{
+				z3::expr child = proofNode.arg(i);
+				if (!visited.count(child.id()))
+				{
+					visited.insert(child.id());
+					proofStack.push(child);
+				}
+
+				if (!graph.nodes.count(child.id()))
+				{
+					graph.nodes[child.id()] = {name(fact(child)), arguments(fact(child))};
+					graph.edges[child.id()] = {};
+				}
+
+				graph.edges[proofNode.id()].push_back(child.id());
+			}
+		}
+	}
+
+	return graph;
+}
+
+z3::expr Z3CHCInterface::fact(z3::expr const& _node)
+{
+	smtAssert(_node.is_app(), "");
+	if (_node.num_args() == 0)
+		return _node;
+	return _node.arg(_node.num_args() - 1);
+}
+
+string Z3CHCInterface::name(z3::expr const& _predicate)
+{
+	smtAssert(_predicate.is_app(), "");
+	return _predicate.decl().name().str();
+}
+
+vector<string> Z3CHCInterface::arguments(z3::expr const& _predicate)
+{
+	smtAssert(_predicate.is_app(), "");
+	vector<string> args;
+	for (unsigned i = 0; i < _predicate.num_args(); ++i)
+		args.emplace_back(_predicate.arg(i).to_string());
+	return args;
 }

libsmtutil/Z3CHCInterface.h

@@ -25,6 +25,8 @@
 #include <libsmtutil/CHCSolverInterface.h>
 #include <libsmtutil/Z3Interface.h>
 
+#include <vector>
+
 namespace solidity::smtutil
 {
 
@@ -40,11 +42,22 @@ public:
 
 	void addRule(Expression const& _expr, std::string const& _name) override;
 
-	std::pair<CheckResult, std::vector<std::string>> query(Expression const& _expr) override;
+	std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
 
 	Z3Interface* z3Interface() const { return m_z3Interface.get(); }
 
+	void setSpacerOptions(bool _preProcessing = true);
+
 private:
+	/// Constructs a nonlinear counterexample graph from the refutation.
+	CHCSolverInterface::CexGraph cexGraph(z3::expr const& _proof);
+	/// @returns the fact from a proof node.
+	z3::expr fact(z3::expr const& _node);
+	/// @returns @a _predicate's name.
+	std::string name(z3::expr const& _predicate);
+	/// @returns the arguments of @a _predicate.
+	std::vector<std::string> arguments(z3::expr const& _predicate);
+
 	// Used to handle variables.
 	std::unique_ptr<Z3Interface> m_z3Interface;
 

libsolidity/formal/CHC.cpp

@@ -29,6 +29,11 @@
 #include <libsmtutil/CHCSmtLib2Interface.h>
 #include <libsolutil/Algorithms.h>
 
+#include <boost/algorithm/string/join.hpp>
+#include <boost/range/adaptor/reversed.hpp>
+
+#include <queue>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
@@ -122,6 +127,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 	string suffix = _contract.name() + "_" + to_string(_contract.id());
 	m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_" + suffix);
 	m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix);
+	m_symbolFunction[m_constructorSummaryPredicate->currentFunctionValue().name] = &_contract;
 	m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix);
 	auto stateExprs = currentStateVariables();
 	setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
@@ -142,12 +148,11 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	else
 		inlineConstructorHierarchy(_contract);
 
-	auto summary = predicate(*m_constructorSummaryPredicate, vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables());
-	connectBlocks(m_currentBlock, summary);
+	connectBlocks(m_currentBlock, summary(_contract), m_error.currentValue() == 0);
 
 	clearIndices(m_currentContract, nullptr);
-	auto stateExprs = vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
-	setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
+	vector<smtutil::Expression> symbArgs = currentFunctionVariables(*m_currentContract);
+	setCurrentBlock(*m_constructorSummaryPredicate, &symbArgs);
 
 	addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), m_error.currentValue());
 	connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
@@ -209,6 +214,8 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	if (!_function.isImplemented())
 		return;
 
+	solAssert(m_currentFunction && m_currentContract, "");
+
 	// This is the case for base constructor inlining.
 	if (m_currentFunction != &_function)
 	{
@@ -228,10 +235,10 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		{
 			string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
 			auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix);
-			connectBlocks(m_currentBlock, predicate(*constructorExit, vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables()));
+			connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract)));
 
 			clearIndices(m_currentContract, m_currentFunction);
-			auto stateExprs = vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
+			auto stateExprs = currentFunctionVariables(*m_currentContract);
 			setCurrentBlock(*constructorExit, &stateExprs);
 		}
 		else
@@ -564,6 +571,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 			m_context.variable(*var)->increaseIndex();
 
 	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
+	m_symbolFunction[nondet.name] = &_funCall;
 	m_context.addAssertion(nondet);
 
 	m_context.addAssertion(m_error.currentValue() == 0);
@@ -613,6 +621,7 @@ void CHC::resetSourceAnalysis()
 	m_errorIds.clear();
 	m_callGraph.clear();
 	m_summaries.clear();
+	m_symbolFunction.clear();
 }
 
 void CHC::resetContractAnalysis()
@@ -683,6 +692,11 @@ vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPriva
 	);
 }
 
+vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
+{
+	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
+}
+
 vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
 {
 	return applyMap(
@@ -693,6 +707,10 @@ vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract
 
 smtutil::SortPointer CHC::constructorSort()
 {
+	solAssert(m_currentContract, "");
+	if (auto const* constructor = m_currentContract->constructor())
+		return sort(*constructor);
+
 	return make_shared<smtutil::FunctionSort>(
 		vector<smtutil::SortPointer>{smtutil::SortProvider::uintSort} + m_stateSorts,
 		smtutil::SortProvider::boolSort
@@ -835,7 +853,12 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 
 					m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
 
-					if (!base->isLibrary() && !base->isInterface() && !function->isConstructor())
+					if (
+						!function->isConstructor() &&
+						function->isPublic() &&
+						!base->isLibrary() &&
+						!base->isInterface()
+					)
 					{
 						auto state1 = stateVariablesAtIndex(1, *base);
 						auto state2 = stateVariablesAtIndex(2, *base);
@@ -880,8 +903,13 @@ smtutil::Expression CHC::error(unsigned _idx)
 	return m_errorPredicate->functionValueAtIndex(_idx)({});
 }
 
-smtutil::Expression CHC::summary(ContractDefinition const&)
+smtutil::Expression CHC::summary(ContractDefinition const& _contract)
 {
+	if (auto const* constructor = _contract.constructor())
+		return (*m_constructorSummaryPredicate)(
+			currentFunctionVariables(*constructor)
+		);
+
 	return (*m_constructorSummaryPredicate)(
 		vector<smtutil::Expression>{m_error.currentValue()} +
 		currentStateVariables()
@@ -908,21 +936,28 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function)
 
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
 {
-	return createSymbolicBlock(sort(_node),
+	auto block = createSymbolicBlock(sort(_node),
 		"block_" +
 		uniquePrefix() +
 		"_" +
 		_prefix +
 		predicateName(_node));
+
+	solAssert(m_currentFunction, "");
+	m_symbolFunction[block->currentFunctionValue().name] = m_currentFunction;
+	return block;
 }
 
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
-	return createSymbolicBlock(summarySort(_function, _contract),
+	auto block = createSymbolicBlock(summarySort(_function, _contract),
 		"summary_" +
 		uniquePrefix() +
 		"_" +
 		predicateName(&_function, &_contract));
+
+	m_symbolFunction[block->currentFunctionValue().name] = &_function;
+	return block;
 }
 
 void CHC::createErrorBlock()
@@ -977,15 +1012,21 @@ vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const&
 }
 
 vector<smtutil::Expression> CHC::currentFunctionVariables()
+{
+	solAssert(m_currentFunction, "");
+	return currentFunctionVariables(*m_currentFunction);
+}
+
+vector<smtutil::Expression> CHC::currentFunctionVariables(FunctionDefinition const& _function)
 {
 	vector<smtutil::Expression> initInputExprs;
 	vector<smtutil::Expression> mutableInputExprs;
-	for (auto const& var: m_currentFunction->parameters())
+	for (auto const& var: _function.parameters())
 	{
 		initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0));
 		mutableInputExprs.push_back(m_context.variable(*var)->currentValue());
 	}
-	auto returnExprs = applyMap(m_currentFunction->returnParameters(), [this](auto _var) { return currentValue(*_var); });
+	auto returnExprs = applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); });
 	return vector<smtutil::Expression>{m_error.currentValue()} +
 		initialStateVariables() +
 		initInputExprs +
@@ -994,6 +1035,14 @@ vector<smtutil::Expression> CHC::currentFunctionVariables()
 		returnExprs;
 }
 
+vector<smtutil::Expression> CHC::currentFunctionVariables(ContractDefinition const& _contract)
+{
+	if (auto const* constructor = _contract.constructor())
+		return currentFunctionVariables(*constructor);
+
+	return vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
+}
+
 vector<smtutil::Expression> CHC::currentBlockVariables()
 {
 	if (m_currentFunction)
@@ -1074,15 +1123,33 @@ void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)
 	m_interface->addRule(_rule, _ruleName);
 }
 
-pair<smtutil::CheckResult, vector<string>> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
+pair<smtutil::CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
 {
 	smtutil::CheckResult result;
-	vector<string> values;
-	tie(result, values) = m_interface->query(_query);
+	CHCSolverInterface::CexGraph cex;
+	tie(result, cex) = m_interface->query(_query);
 	switch (result)
 	{
 	case smtutil::CheckResult::SATISFIABLE:
+	{
+#ifdef HAVE_Z3
+		// Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete.
+		// We now disable those optimizations and check whether we can still solve the problem.
+		auto* spacer = dynamic_cast<Z3CHCInterface*>(m_interface.get());
+		solAssert(spacer, "");
+		spacer->setSpacerOptions(false);
+
+		smtutil::CheckResult resultNoOpt;
+		CHCSolverInterface::CexGraph cexNoOpt;
+		tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);
+
+		if (resultNoOpt == smtutil::CheckResult::SATISFIABLE)
+			cex = move(cexNoOpt);
+
+		spacer->setSpacerOptions(true);
+#endif
 		break;
+	}
 	case smtutil::CheckResult::UNSATISFIABLE:
 		break;
 	case smtutil::CheckResult::UNKNOWN:
@@ -1094,7 +1161,7 @@ pair<smtutil::CheckResult, vector<string>> CHC::query(smtutil::Expression const&
 		m_outerErrorReporter.warning(1218_error, _location, "Error trying to invoke SMT solver.");
 		break;
 	}
-	return {result, values};
+	return {result, cex};
 }
 
 void CHC::addVerificationTarget(
@@ -1138,19 +1205,21 @@ void CHC::checkVerificationTargets()
 		{
 			string satMsg;
 			string unknownMsg;
+			ErrorId errorReporterId;
 
 			if (target.type == VerificationTarget::Type::PopEmptyArray)
 			{
 				solAssert(dynamic_cast<FunctionCall const*>(scope), "");
-				satMsg = "Empty array \"pop\" detected here.";
+				satMsg = "Empty array \"pop\" detected here";
 				unknownMsg = "Empty array \"pop\" might happen here.";
+				errorReporterId = 2529_error;
 			}
 			else
 				solAssert(false, "");
 
 			auto it = m_errorIds.find(scope->id());
 			solAssert(it != m_errorIds.end(), "");
-			checkAndReportTarget(scope, target, it->second, satMsg, unknownMsg);
+			checkAndReportTarget(scope, target, it->second, errorReporterId, satMsg, unknownMsg);
 		}
 	}
 }
@@ -1165,13 +1234,7 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const&
 		solAssert(it != m_errorIds.end(), "");
 		unsigned errorId = it->second;
 
-		createErrorBlock();
-		connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == errorId));
-		auto [result, model] = query(error(), assertion->location());
-		// This should be fine but it's a bug in the old compiler
-		(void)model;
-		if (result == smtutil::CheckResult::UNSATISFIABLE)
-			m_safeTargets[assertion].insert(_target.type);
+		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here");
 	}
 }
 
@@ -1179,35 +1242,251 @@ void CHC::checkAndReportTarget(
 	ASTNode const* _scope,
 	CHCVerificationTarget const& _target,
 	unsigned _errorId,
+	ErrorId _errorReporterId,
 	string _satMsg,
 	string _unknownMsg
 )
 {
+	if (m_unsafeTargets.count(_scope) && m_unsafeTargets.at(_scope).count(_target.type))
+		return;
+
 	createErrorBlock();
 	connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == _errorId));
-	auto [result, model] = query(error(), _scope->location());
-	// This should be fine but it's a bug in the old compiler
-	(void)model;
+	auto const& [result, model] = query(error(), _scope->location());
 	if (result == smtutil::CheckResult::UNSATISFIABLE)
 		m_safeTargets[_scope].insert(_target.type);
 	else if (result == smtutil::CheckResult::SATISFIABLE)
 	{
 		solAssert(!_satMsg.empty(), "");
 		m_unsafeTargets[_scope].insert(_target.type);
-		m_outerErrorReporter.warning(
-			2529_error,
-			_scope->location(),
-			_satMsg
-		);
+		auto cex = generateCounterexample(model, error().name);
+		if (cex)
+			m_outerErrorReporter.warning(
+				_errorReporterId,
+				_scope->location(),
+				_satMsg,
+				SecondarySourceLocation().append(" for:\n" + *cex, SourceLocation{})
+			);
+		else
+			m_outerErrorReporter.warning(
+				_errorReporterId,
+				_scope->location(),
+				_satMsg + "."
+			);
 	}
 	else if (!_unknownMsg.empty())
 		m_outerErrorReporter.warning(
-			1147_error,
+			_errorReporterId,
 			_scope->location(),
 			_unknownMsg
 		);
 }
 
+/**
+The counterexample DAG has the following properties:
+1) The root node represents the reachable error predicate.
+2) The root node has 1 or 2 children:
+	- One of them is the summary of the function that was called and led to that node.
+	If this is the only child, this function must be the constructor.
+	- If it has 2 children, the function is not the constructor and the other child is the interface node,
+	that is, it represents the state of the contract before the function described above was called.
+3) Interface nodes also have property 2.
+
+The following algorithm starts collecting function summaries at the root node and repeats
+for each interface node seen.
+Each function summary collected represents a transaction, and the final order is reversed.
+
+The first function summary seen contains the values for the state, input and output variables at the
+error point.
+*/
+optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const& _graph, string const& _root)
+{
+	optional<unsigned> rootId;
+	for (auto const& [id, node]: _graph.nodes)
+		if (node.first == _root)
+		{
+			rootId = id;
+			break;
+		}
+	if (!rootId)
+		return {};
+
+	vector<string> path;
+	string localState;
+
+	unsigned node = *rootId;
+	/// The first summary node seen in this loop represents the last transaction.
+	bool lastTxSeen = false;
+	while (_graph.edges.at(node).size() >= 1)
+	{
+		auto const& edges = _graph.edges.at(node);
+		solAssert(edges.size() <= 2, "");
+
+		unsigned summaryId = edges.at(0);
+
+		optional<unsigned> interfaceId;
+		if (edges.size() == 2)
+		{
+			interfaceId = edges.at(1);
+			if (_graph.nodes.at(summaryId).first.rfind("summary", 0) != 0)
+				swap(summaryId, *interfaceId);
+			solAssert(_graph.nodes.at(*interfaceId).first.rfind("interface", 0) == 0, "");
+		}
+		/// The children are unordered, so we need to check which is the summary and
+		/// which is the interface.
+
+		solAssert(_graph.nodes.at(summaryId).first.rfind("summary", 0) == 0, "");
+		/// At this point property 2 from the function description is verified for this node.
+
+		auto const& summaryNode = _graph.nodes.at(summaryId);
+		solAssert(m_symbolFunction.count(summaryNode.first), "");
+
+		FunctionDefinition const* calledFun = nullptr;
+		ContractDefinition const* calledContract = nullptr;
+		if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_symbolFunction.at(summaryNode.first)))
+		{
+			if (auto const* constructor = contract->constructor())
+				calledFun = constructor;
+			else
+				calledContract = contract;
+		}
+		else if (auto const* fun = dynamic_cast<FunctionDefinition const*>(m_symbolFunction.at(summaryNode.first)))
+			calledFun = fun;
+		else
+			solAssert(false, "");
+
+		solAssert((calledFun && !calledContract) || (!calledFun && calledContract), "");
+		auto const& stateVars = calledFun ? stateVariablesIncludingInheritedAndPrivate(*calledFun) : stateVariablesIncludingInheritedAndPrivate(*calledContract);
+		/// calledContract != nullptr implies that the constructor of the analyzed contract is implicit and
+		/// therefore takes no parameters.
+
+		/// This summary node is the end of a tx.
+		/// If it is the first summary node seen in this loop, it is the summary
+		/// of the public/external function that was called when the error was reached,
+		/// but not necessarily the summary of the function that contains the error.
+		if (!lastTxSeen)
+		{
+			lastTxSeen = true;
+			/// Generate counterexample message local to the failed target.
+			localState = formatStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n";
+			if (calledFun)
+			{
+				/// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
+				auto const& inParams = calledFun->parameters();
+				unsigned initLocals = stateVars.size() * 2 + 1 + inParams.size();
+				/// In this loop we are interested in postInputVars.
+				for (unsigned i = initLocals; i < initLocals + inParams.size(); ++i)
+				{
+					auto param = inParams.at(i - initLocals);
+					if (param->type()->isValueType())
+						localState += param->name() + " = " + summaryNode.second.at(i) + "\n";
+				}
+				auto const& outParams = calledFun->returnParameters();
+				initLocals += inParams.size();
+				/// In this loop we are interested in outputVars.
+				for (unsigned i = initLocals; i < initLocals + outParams.size(); ++i)
+				{
+					auto param = outParams.at(i - initLocals);
+					if (param->type()->isValueType())
+						localState += param->name() + " = " + summaryNode.second.at(i) + "\n";
+				}
+			}
+		}
+		else
+			/// We report the state after every tx in the trace except for the last, which is reported
+			/// first in the code above.
+			path.emplace_back("State: " + formatStateCounterexample(stateVars, calledFun, summaryNode.second));
+
+		string txCex = calledContract ? "constructor()" : formatFunctionCallCounterexample(stateVars, *calledFun, summaryNode.second);
+		path.emplace_back(txCex);
+
+		/// Recurse on the next interface node which represents the previous transaction
+		/// or stop.
+		if (interfaceId)
+			node = *interfaceId;
+		else
+			break;
+	}
+
+	return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
+}
+
+string CHC::formatStateCounterexample(vector<VariableDeclaration const*> const& _stateVars, FunctionDefinition const* _function, vector<string> const& _summaryValues)
+{
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
+	/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
+	/// Here we are interested in postStateVars.
+	vector<string>::const_iterator stateFirst;
+	vector<string>::const_iterator stateLast;
+	if (_function)
+	{
+		stateFirst = _summaryValues.begin() + 1 + static_cast<int>(_stateVars.size()) + static_cast<int>(_function->parameters().size());
+		stateLast = stateFirst + static_cast<int>(_stateVars.size());
+	}
+	else
+	{
+		stateFirst = _summaryValues.begin() + 1;
+		stateLast = stateFirst + static_cast<int>(_stateVars.size());
+	}
+
+	solAssert(stateFirst >= _summaryValues.begin() && stateFirst <= _summaryValues.end(), "");
+	solAssert(stateLast >= _summaryValues.begin() && stateLast <= _summaryValues.end(), "");
+	vector<string> stateArgs(stateFirst, stateLast);
+	solAssert(stateArgs.size() == _stateVars.size(), "");
+
+	vector<string> stateCex;
+	for (unsigned i = 0; i < stateArgs.size(); ++i)
+	{
+		auto var = _stateVars.at(i);
+		if (var->type()->isValueType())
+			stateCex.emplace_back(var->name() + " = " + stateArgs.at(i));
+	}
+
+	return boost::algorithm::join(stateCex, ", ");
+}
+
+string CHC::formatFunctionCallCounterexample(vector<VariableDeclaration const*> const& _stateVars, FunctionDefinition const& _function, vector<string> const& _summaryValues)
+{
+	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
+	/// Here we are interested in preInputVars.
+	vector<string>::const_iterator first = _summaryValues.begin() + static_cast<int>(_stateVars.size()) + 1;
+	vector<string>::const_iterator last = first + static_cast<int>(_function.parameters().size());
+	solAssert(first >= _summaryValues.begin() && first <= _summaryValues.end(), "");
+	solAssert(last >= _summaryValues.begin() && last <= _summaryValues.end(), "");
+	vector<string> functionArgsCex(first, last);
+	vector<string> functionArgs;
+
+	auto const& params = _function.parameters();
+	solAssert(params.size() == functionArgsCex.size(), "");
+	for (unsigned i = 0; i < params.size(); ++i)
+		if (params[i]->type()->isValueType())
+			functionArgs.emplace_back(functionArgsCex[i]);
+		else
+			functionArgs.emplace_back(params[i]->name());
+
+	string fName = _function.isConstructor() ? "constructor" :
+		_function.isFallback() ? "fallback" :
+		_function.isReceive() ? "receive" :
+		_function.name();
+	return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
+}
+
+string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
+{
+	string dot = "digraph {\n";
+
+	auto pred = [&](CHCSolverInterface::CexNode const& _node) {
+		return "\"" + _node.first + "(" + boost::algorithm::join(_node.second, ", ") + ")\"";
+	};
+
+	for (auto const& [u, vs]: _cex.edges)
+		for (auto v: vs)
+			dot += pred(_cex.nodes.at(v)) + " -> " + pred(_cex.nodes.at(u)) + "\n";
+
+	dot += "}";
+	return dot;
+}
+
 string CHC::uniquePrefix()
 {
 	return to_string(m_blockCounter++);

libsolidity/formal/CHC.h

@@ -38,6 +38,7 @@
 #include <libsmtutil/CHCSolverInterface.h>
 
 #include <map>
+#include <optional>
 #include <set>
 
 namespace solidity::frontend
@@ -102,6 +103,7 @@ private:
 	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
 	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
+	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
 	//@}
 
 	/// Sort helpers.
@@ -164,6 +166,9 @@ private:
 	/// @returns the current symbolic values of the current function's
 	/// input and output parameters.
 	std::vector<smtutil::Expression> currentFunctionVariables();
+	std::vector<smtutil::Expression> currentFunctionVariables(FunctionDefinition const& _function);
+	std::vector<smtutil::Expression> currentFunctionVariables(ContractDefinition const& _contract);
+
 	/// @returns the same as currentFunctionVariables plus
 	/// local variables.
 	std::vector<smtutil::Expression> currentBlockVariables();
@@ -189,7 +194,7 @@ private:
 	void addRule(smtutil::Expression const& _rule, std::string const& _ruleName);
 	/// @returns <true, empty> if query is unsatisfiable (safe).
 	/// @returns <false, model> otherwise.
-	std::pair<smtutil::CheckResult, std::vector<std::string>> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
+	std::pair<smtutil::CheckResult, smtutil::CHCSolverInterface::CexGraph> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
 
 	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
 	void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
@@ -203,9 +208,25 @@ private:
 		ASTNode const* _scope,
 		CHCVerificationTarget const& _target,
 		unsigned _errorId,
+		langutil::ErrorId _errorReporterId,
 		std::string _satMsg,
-		std::string _unknownMsg
+		std::string _unknownMsg = ""
 	);
+
+	std::optional<std::string> generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root);
+	/// @returns values for the _stateVariables after a transaction calling
+	/// _function was executed.
+	/// _function = nullptr means the transaction was the deployment of a
+	/// contract without an explicit constructor.
+	std::string formatStateCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const* _function, std::vector<std::string> const& _summaryValues);
+	/// @returns a formatted text representing a call to _function
+	/// with the concrete values for value type parameters and
+	/// the parameter name for reference types.
+	std::string formatFunctionCallCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const& _function, std::vector<std::string> const& _summaryValues);
+
+	/// @returns a DAG in the dot format.
+	/// Used for debugging purposes.
+	std::string cex2dot(smtutil::CHCSolverInterface::CexGraph const& _graph);
 	//@}
 
 	/// Misc.
@@ -255,6 +276,9 @@ private:
 		"error",
 		m_context
 	};
+
+	/// Maps predicate names to the ASTNodes they came from.
+	std::map<std::string, ASTNode const*> m_symbolFunction;
 	//@}
 
 	/// Variables.

test/InteractiveTests.h

@@ -67,7 +67,6 @@ Testsuite const g_interactiveTestsuites[] = {
 	{"JSON AST",            "libsolidity", "ASTJSON",             false, false, &ASTJSONTest::create},
 	{"JSON ABI",            "libsolidity", "ABIJson",             false, false, &ABIJsonTest::create},
 	{"SMT Checker",         "libsolidity", "smtCheckerTests",     true,  false, &SMTCheckerTest::create, {"nooptions"}},
-	{"SMT Checker JSON",    "libsolidity", "smtCheckerTestsJSON", true,  false, &SMTCheckerJSONTest::create, {"nooptions"}},
 	{"Gas Estimates",       "libsolidity", "gasTests",            false, false, &GasTest::create}
 };
 

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol

@@ -11,10 +11,10 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (119-157): Assertion violation happens here
 // Warning 8115: (76-80): Assertion checker does not yet support the type of this variable.
 // Warning 8115: (83-87): Assertion checker does not yet support the type of this variable.
 // Warning 7650: (126-132): Assertion checker does not yet support this expression.
 // Warning 8364: (126-128): Assertion checker does not yet implement type struct C.S storage ref
 // Warning 7650: (143-149): Assertion checker does not yet support this expression.
 // Warning 8364: (143-145): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 4661: (119-157): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol

@@ -11,6 +11,7 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (121-165): Assertion violation happens here
 // Warning 8115: (78-82): Assertion checker does not yet support the type of this variable.
 // Warning 8115: (85-89): Assertion checker does not yet support the type of this variable.
 // Warning 7650: (128-134): Assertion checker does not yet support this expression.
@@ -19,4 +20,3 @@ contract C {
 // Warning 7650: (148-154): Assertion checker does not yet support this expression.
 // Warning 8364: (148-150): Assertion checker does not yet implement type struct C.S storage ref
 // Warning 9118: (148-157): Assertion checker does not yet implement this expression.
-// Warning 4661: (121-165): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_basic.sol

@@ -10,4 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (153-176): Assertion violation happens here
+// Warning 6328: (153-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol

@@ -14,6 +14,6 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (198-224): Assertion violation happens here
-// Warning 4661: (228-254): Assertion violation happens here
-// Warning 4661: (258-281): Assertion violation happens here
+// Warning 6328: (198-224): Assertion violation happens here
+// Warning 6328: (228-254): Assertion violation happens here
+// Warning 6328: (258-281): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol

@@ -16,7 +16,7 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (222-248): Assertion violation happens here
-// Warning 4661: (252-278): Assertion violation happens here
-// Warning 4661: (282-305): Assertion violation happens here
-// Warning 4661: (309-335): Assertion violation happens here
+// Warning 6328: (222-248): Assertion violation happens here
+// Warning 6328: (252-278): Assertion violation happens here
+// Warning 6328: (282-305): Assertion violation happens here
+// Warning 6328: (309-335): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): Empty array "pop" detected here.
+// Warning 2529: (82-89): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (111-121): Empty array "pop" detected here.
+// Warning 2529: (111-121): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (76-83): Empty array "pop" detected here.
+// Warning 2529: (76-83): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (150-157): Empty array "pop" detected here.
+// Warning 2529: (150-157): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol

@@ -10,5 +10,5 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (150-184): Assertion violation happens here
 // Warning 4144: (162-177): Underflow (resulting value less than 0) happens here
-// Warning 4661: (150-184): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol

@@ -8,5 +8,5 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (113-139): Assertion violation happens here
-// Warning 4661: (143-189): Assertion violation happens here
+// Warning 6328: (113-139): Assertion violation happens here
+// Warning 6328: (143-189): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol

@@ -10,6 +10,6 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (122-148): Assertion violation happens here
-// Warning 4661: (202-218): Assertion violation happens here
-// Warning 4661: (222-278): Assertion violation happens here
+// Warning 6328: (122-148): Assertion violation happens here
+// Warning 6328: (202-218): Assertion violation happens here
+// Warning 6328: (222-278): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol

@@ -12,5 +12,5 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (205-239): Assertion violation happens here
 // Warning 4144: (217-232): Underflow (resulting value less than 0) happens here
-// Warning 4661: (205-239): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol

@@ -12,4 +12,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (167-188): Assertion violation happens here
+// Warning 6328: (167-188): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol

@@ -18,6 +18,6 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (193-217): Assertion violation happens here
-// Warning 4661: (309-333): Assertion violation happens here
-// Warning 4661: (419-436): Assertion violation happens here
+// Warning 6328: (193-217): Assertion violation happens here
+// Warning 6328: (309-333): Assertion violation happens here
+// Warning 6328: (419-436): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (111-144): Assertion violation happens here
+// Warning 6328: (111-144): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (94-124): Assertion violation happens here
+// Warning 6328: (94-124): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol

@@ -15,4 +15,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (184-213): Assertion violation happens here
+// Warning 6328: (184-213): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol

@@ -15,5 +15,5 @@ contract c {
 	}
 }
 // ----
+// Warning 6328: (227-236): Assertion violation happens here
 // Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (227-236): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol

@@ -17,6 +17,6 @@ contract c {
 	}
 }
 // ----
+// Warning 6328: (202-218): Assertion violation happens here
+// Warning 6328: (242-252): Assertion violation happens here
 // Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (202-218): Assertion violation happens here
-// Warning 4661: (242-252): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol

@@ -15,5 +15,5 @@ contract c {
 	}
 }
 // ----
+// Warning 6328: (225-235): Assertion violation happens here
 // Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol

@@ -15,5 +15,5 @@ contract c {
 	}
 }
 // ----
+// Warning 6328: (225-235): Assertion violation happens here
 // Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol

@@ -24,5 +24,5 @@ contract c {
 	}
 }
 // ----
+// Warning 6328: (360-370): Assertion violation happens here
 // Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (360-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol

@@ -15,5 +15,5 @@ contract c {
 	}
 }
 // ----
+// Warning 6328: (225-235): Assertion violation happens here
 // Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 4661: (159-173): Assertion violation happens here
+// Warning 6328: (159-173): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 4661: (159-173): Assertion violation happens here
+// Warning 6328: (159-173): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 4661: (161-175): Assertion violation happens here
+// Warning 6328: (161-175): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external.sol

@@ -17,4 +17,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (200-214): Assertion violation happens here
+// Warning 6328: (200-214): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash.sol

@@ -26,4 +26,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (423-445): Assertion violation happens here
+// Warning 6328: (423-445): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol

@@ -28,4 +28,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (431-453): Assertion violation happens here
+// Warning 6328: (431-453): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol

@@ -34,5 +34,5 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (528-565): Assertion violation happens here
 // Warning 5084: (544-554): Type conversion is not yet fully supported and might yield false positives.
-// Warning 4661: (528-565): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -29,4 +29,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (299-313): Assertion violation happens here
+// Warning 6328: (299-313): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol

@@ -42,6 +42,6 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (452-466): Assertion violation happens here
+// Warning 6328: (470-496): Assertion violation happens here
 // Warning 5084: (92-102): Type conversion is not yet fully supported and might yield false positives.
-// Warning 4661: (452-466): Assertion violation happens here
-// Warning 4661: (470-496): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol

@@ -34,6 +34,6 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (381-395): Assertion violation happens here
+// Warning 6328: (399-425): Assertion violation happens here
 // Warning 5084: (116-126): Type conversion is not yet fully supported and might yield false positives.
-// Warning 4661: (381-395): Assertion violation happens here
-// Warning 4661: (399-425): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol

@@ -38,6 +38,6 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (435-461): Assertion violation happens here
+// Warning 6328: (435-461): Assertion violation happens here
+// Warning 6328: (594-631): Assertion violation happens here
 // Warning 5084: (610-620): Type conversion is not yet fully supported and might yield false positives.
-// Warning 4661: (594-631): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_inc.sol

@@ -18,5 +18,5 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (189-203): Assertion violation happens here
 // Warning 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (189-203): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol

@@ -25,4 +25,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (286-303): Assertion violation happens here
+// Warning 6328: (286-303): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol

@@ -23,4 +23,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (256-273): Assertion violation happens here
+// Warning 6328: (256-273): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol

@@ -27,4 +27,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (307-321): Assertion violation happens here
+// Warning 6328: (307-321): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol

@@ -13,4 +13,4 @@ contract A is C {
 	}
 }
 // ----
-// Warning 4661: (152-166): Assertion violation happens here
+// Warning 6328: (152-166): Assertion violation happens here

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 4661: (243-257): Assertion violation happens here
+// Warning 6328: (243-257): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol

@@ -19,6 +19,6 @@ contract A is B {
 	}
 }
 // ----
+// Warning 6328: (232-250): Assertion violation happens here
 // Warning 2661: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (244-249): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (232-250): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol

@@ -25,7 +25,7 @@ contract A is B2, B1 {
 	}
 }
 // ----
+// Warning 6328: (302-320): Assertion violation happens here
 // Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (302-320): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol

@@ -25,7 +25,7 @@ contract A is B2, B1 {
 	}
 }
 // ----
+// Warning 6328: (302-320): Assertion violation happens here
 // Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (302-320): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol

@@ -27,6 +27,7 @@ contract A is B2, B1 {
 	}
 }
 // ----
+// Warning 6328: (334-350): Assertion violation happens here
 // Warning 4144: (160-165): Underflow (resulting value less than 0) happens here
 // Warning 2661: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here
@@ -34,4 +35,3 @@ contract A is B2, B1 {
 // Warning 2661: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (334-350): 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 4661: (194-208): Assertion violation happens here
+// Warning 6328: (194-208): Assertion violation happens here

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 4661: (224-238): Assertion violation happens here
+// Warning 6328: (224-238): Assertion violation happens here

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 4661: (172-186): Assertion violation happens here
+// Warning 6328: (172-186): Assertion violation happens here

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 4661: (150-164): Assertion violation happens here
+// Warning 6328: (150-164): Assertion violation happens here

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 4661: (284-298): Assertion violation happens here
+// Warning 6328: (284-298): Assertion violation happens here

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 4661: (357-372): Assertion violation happens here
+// Warning 6328: (357-372): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol

@@ -25,6 +25,6 @@ contract A is B {
 	}
 }
 // ----
+// Warning 6328: (328-342): Assertion violation happens here
 // Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (328-342): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol

@@ -23,5 +23,4 @@ contract B is C {
 contract A is B {
 }
 // ----
-// Warning 4661: (266-280): Assertion violation happens here
-// Warning 4661: (266-280): Assertion violation happens here
+// Warning 6328: (266-280): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol

@@ -14,4 +14,4 @@ contract A is C {
 	}
 }
 // ----
-// Warning 4661: (188-202): Assertion violation happens here
+// Warning 6328: (188-202): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol

@@ -13,5 +13,5 @@ contract A is C {
 	}
 }
 // ----
-// Warning 4661: (134-148): Assertion violation happens here
-// Warning 4661: (152-168): Assertion violation happens here
+// Warning 6328: (134-148): Assertion violation happens here
+// Warning 6328: (152-168): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_simple.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (141-155): Assertion violation happens here
+// Warning 6328: (141-155): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (145-159): Assertion violation happens here
+// Warning 6328: (145-159): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol

@@ -15,4 +15,4 @@ contract C is B {
 	}
 }
 // ----
-// Warning 4661: (165-179): Assertion violation happens here
+// Warning 6328: (165-179): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol

@@ -13,5 +13,5 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (162-176): Assertion violation happens here
+// Warning 6328: (162-176): Assertion violation happens here
 // Warning 2661: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/functions/function_call_state_var_init.sol

@@ -9,5 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (116-132): Assertion violation happens here
-// Warning 4661: (116-132): Assertion violation happens here
+// Warning 6328: (116-132): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol

@@ -16,4 +16,4 @@ contract C
 	}
 }
 // ----
-// Warning 4661: (209-223): Assertion violation happens here
+// Warning 6328: (209-223): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol

@@ -24,5 +24,5 @@ contract C
 
 }
 // ----
-// Warning 4661: (209-223): Assertion violation happens here
-// Warning 4661: (321-335): Assertion violation happens here
+// Warning 6328: (209-223): Assertion violation happens here
+// Warning 6328: (321-335): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol

@@ -18,4 +18,4 @@ contract C
 	}
 }
 // ----
-// Warning 4661: (261-277): Assertion violation happens here
+// Warning 6328: (261-277): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_4.sol

@@ -16,4 +16,4 @@ contract D
 	}
 }
 // ----
-// Warning 4661: (191-206): Assertion violation happens here
+// Warning 6328: (191-206): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol

@@ -12,4 +12,4 @@ contract C
 }
 
 // ----
-// Warning 4661: (161-174): Assertion violation happens here
+// Warning 6328: (161-174): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol

@@ -16,4 +16,4 @@ contract C
 }
 
 // ----
-// Warning 4661: (229-242): Assertion violation happens here
+// Warning 6328: (229-242): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol

@@ -12,4 +12,4 @@ contract C
 }
 
 // ----
-// Warning 4661: (163-176): Assertion violation happens here
+// Warning 6328: (163-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol

@@ -17,5 +17,5 @@ contract C
 	}
 }
 // ----
+// Warning 6328: (245-261): Assertion violation happens here
 // Warning 8364: (228-229): Assertion checker does not yet implement type type(library L)
-// Warning 4661: (245-261): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol

@@ -13,4 +13,4 @@ contract C
 }
 
 // ----
-// Warning 4661: (144-157): Assertion violation happens here
+// Warning 6328: (144-157): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol

@@ -14,4 +14,4 @@ contract C
 }
 
 // ----
-// Warning 4661: (152-165): Assertion violation happens here
+// Warning 6328: (152-165): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol

@@ -17,4 +17,4 @@ contract A is B {
 	}
 }
 // ----
-// Warning 4661: (254-268): Assertion violation happens here
+// Warning 6328: (254-268): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol

@@ -21,4 +21,4 @@ contract A is B {
 	}
 }
 // ----
-// Warning 4661: (274-288): Assertion violation happens here
+// Warning 6328: (274-288): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol

@@ -21,12 +21,10 @@ contract C{
 }
 // ----
 // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 4661: (138-152): Assertion violation happens here
+// Warning 6328: (138-152): Assertion violation happens here
+// Warning 6328: (170-184): Assertion violation happens here
+// Warning 6328: (220-234): Assertion violation happens here
+// Warning 6328: (245-259): Assertion violation happens here
+// Warning 6328: (82-96): Assertion violation happens here
 // Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (220-234): Assertion violation happens here
-// Warning 4661: (245-259): Assertion violation happens here
-// Warning 4661: (170-184): Assertion violation happens here
-// Warning 4661: (220-234): Assertion violation happens here
 // Warning 4144: (238-241): Underflow (resulting value less than 0) happens here
-// Warning 4661: (245-259): Assertion violation happens here
-// Warning 4661: (82-96): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1_fail.sol

@@ -17,10 +17,8 @@ contract C is A {
 	}
 }
 // ----
-// Warning 4661: (82-96): Assertion violation happens here
+// Warning 6328: (82-96): Assertion violation happens here
+// Warning 6328: (148-162): Assertion violation happens here
+// Warning 6328: (180-194): Assertion violation happens here
 // Warning 4144: (100-103): Underflow (resulting value less than 0) happens here
-// Warning 4661: (82-96): Assertion violation happens here
 // Warning 4144: (100-103): Underflow (resulting value less than 0) happens here
-// Warning 4661: (148-162): Assertion violation happens here
-// Warning 4661: (82-96): Assertion violation happens here
-// Warning 4661: (180-194): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol

@@ -21,10 +21,10 @@ contract C{
 }
 // ----
 // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 4661: (138-152): Assertion violation happens here
+// Warning 6328: (138-152): Assertion violation happens here
+// Warning 6328: (184-198): Assertion violation happens here
+// Warning 6328: (82-96): Assertion violation happens here
 // Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (234-237): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (184-198): Assertion violation happens here
 // Warning 4144: (234-237): Underflow (resulting value less than 0) happens here
-// Warning 4661: (82-96): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/library_constant.sol

@@ -19,7 +19,7 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (136-155): Assertion violation happens here
+// Warning 6328: (136-155): Assertion violation happens here
 // Warning 2661: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 8364: (300-302): Assertion checker does not yet implement type type(library l1)
 // Warning 2661: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/functions/this_external_call.sol

@@ -9,6 +9,9 @@ contract C
 	function g(uint y) public {
 		require(y < 1000);
 		this.f(y);
+		// Fails as false positive because CHC does not support `this`.
 		assert(x < 1000);
 	}
 }
+// ----
+// Warning 6328: (227-243): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol

@@ -10,6 +10,9 @@ contract C
 	function g(uint y) public {
 		require(y < 1000);
 		uint z = this.f(y);
+		// Fails as false positive because CHC does not support `this`.
 		assert(z < 1000);
 	}
 }
+// ----
+// Warning 6328: (263-279): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/this_fake.sol

@@ -21,4 +21,4 @@ contract C
 }
 // ----
 // Warning 2319: (160-166): This declaration shadows a builtin symbol.
-// Warning 4661: (268-282): Assertion violation happens here
+// Warning 6328: (268-282): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/this_state.sol

@@ -6,10 +6,12 @@ contract C
     function g() public {
 		x = 0;
         this.h();
-		// Function call is inlined.
+		// Fails as false positive because CHC does not support `this`.
 		assert(x == 2);
     }
     function h() public {
         x = 2;
     }
 }
+// ----
+// Warning 6328: (186-200): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol

@@ -25,6 +25,6 @@ contract A is B {
 	}
 }
 // ----
+// Warning 6328: (328-342): Assertion violation happens here
 // Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (328-342): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 4661: (97-111): Assertion violation happens here
+// Warning 6328: (97-111): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_base.sol

@@ -11,4 +11,4 @@ contract D is C {
 	}
 }
 // ----
-// Warning 4661: (117-131): Assertion violation happens here
+// Warning 6328: (117-131): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain.sol

@@ -19,4 +19,4 @@ contract D is C {
 	}
 }
 // ----
-// Warning 4661: (211-225): Assertion violation happens here
+// Warning 6328: (211-225): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_alternate.sol

@@ -18,4 +18,4 @@ contract D is C {
 	}
 }
 // ----
-// Warning 4661: (185-199): Assertion violation happens here
+// Warning 6328: (185-199): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol

@@ -22,6 +22,7 @@ contract A is B {
 }
 
 // ----
+// Warning 6328: (275-293): Assertion violation happens here
 // Warning 4144: (157-162): Underflow (resulting value less than 0) happens here
 // Warning 2661: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (216-221): Overflow (resulting value larger than 2**256 - 1) happens here
@@ -30,4 +31,3 @@ contract A is B {
 // Warning 2661: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (261-270): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (287-292): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (275-293): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol

@@ -22,10 +22,10 @@ contract A is B {
 }
 
 // ----
+// Warning 6328: (273-291): Assertion violation happens here
 // Warning 2661: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (240-245): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (262-268): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 2661: (285-290): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4661: (273-291): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond.sol

@@ -17,4 +17,4 @@ contract D is B, C {
 	}
 }
 // ----
-// Warning 4661: (162-176): Assertion violation happens here
+// Warning 6328: (162-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol

@@ -19,4 +19,4 @@ contract D is B, C {
 	}
 }
 // ----
-// Warning 4661: (214-228): Assertion violation happens here
+// Warning 6328: (214-228): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/fallback.sol

@@ -21,7 +21,6 @@ contract B is A {
 	}
 }
 // ----
-// Warning 4661: (122-136): Assertion violation happens here
-// Warning 4661: (171-185): Assertion violation happens here
-// Warning 4661: (288-302): Assertion violation happens here
-// Warning 4661: (171-185): Assertion violation happens here
+// Warning 6328: (122-136): Assertion violation happens here
+// Warning 6328: (171-185): Assertion violation happens here
+// Warning 6328: (288-302): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol

@@ -21,8 +21,6 @@ contract B is A {
 	}
 }
 // ----
-// Warning 4661: (114-128): Assertion violation happens here
-// Warning 4661: (163-177): Assertion violation happens here
-// Warning 4661: (289-303): Assertion violation happens here
-// Warning 4661: (114-128): Assertion violation happens here
-// Warning 4661: (163-177): Assertion violation happens here
+// Warning 6328: (114-128): Assertion violation happens here
+// Warning 6328: (163-177): Assertion violation happens here
+// Warning 6328: (289-303): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/functions_1.sol

@@ -19,7 +19,6 @@ contract B is A {
 	}
 }
 // ----
-// Warning 4661: (121-135): Assertion violation happens here
-// Warning 4661: (170-184): Assertion violation happens here
-// Warning 4661: (276-290): Assertion violation happens here
-// Warning 4661: (170-184): Assertion violation happens here
+// Warning 6328: (121-135): Assertion violation happens here
+// Warning 6328: (170-184): Assertion violation happens here
+// Warning 6328: (276-290): Assertion violation happens here