Merge pull request #10813 from ethereum/smt_targets_option

Add CLI and JSON option to select SMTChecker targets

Changelog.md

@@ -5,6 +5,9 @@ Language Features:
 
 Compiler Features:
  * Build system: Update the soljson.js build to emscripten 2.0.12 and boost 1.75.0.
+ * Command Line Interface: New option ``--model-checker-targets`` allows specifying which targets should be checked. The valid options are ``all``, ``constantCondition``,
+   ``underflow``, ``overflow``, ``divByZero``, ``balance``, ``assert``, ``popEmptyArray``, where the default is ``all``. Multiple targets can be chosen at the same time,
+   separated by a comma without spaces: ``underflow,overflow,assert``.
  * Optimizer: Add rule to replace ``iszero(sub(x,y))`` by ``eq(x,y)``.
  * Parser: Report meaningful error if parsing a version pragma failed.
  * SMTChecker: Support ABI functions as uninterpreted functions.
@@ -13,6 +16,9 @@ Compiler Features:
  * SMTChecker: Support try/catch statements.
  * SMTChecker: Output internal and trusted external function calls in a counterexample's transaction trace.
  * SMTChecker: Synthesize untrusted functions called externally.
+ * Standard JSON: New option ``modelCheckerSettings.targets`` allows specifying which targets should be checked. The valid options are ``all``, ``constantCondition``,
+   ``underflow``, ``overflow``, ``divByZero``, ``balance``, ``assert``, ``popEmptyArray``, where the default is ``all``. Multiple targets can be chosen at the same time,
+   separated by a comma without spaces: ``underflow,overflow,assert``.
 
 Bugfixes:
  * Code Generator: Fix length check when decoding malformed error data in catch clause.

docs/security-considerations.rst

@@ -438,8 +438,16 @@ inside ``assert`` statements are always true.  If an assertion failure is
 found, a counterexample is given to the user, showing how the assertion can be
 violated.
 
-The SMTChecker also checks automatically for arithmetic underflow/overflow,
-trivial conditions and unreachable code.
+The other verification targets that the SMTChecker checks at compile time are:
+
+- Arithmetic underflow and overflow (`underflow` and `overflow`).
+- Division by zero (`divByZero`).
+- Trivial conditions and unreachable code (`constantCondition`).
+- Popping an empty array (`popEmptyArray`).
+- Insufficient funds for a transfer (`balance`).
+
+The names after each target above can be used when specifying subsets of targets.
+
 It is currently an experimental feature, therefore in order to use it you need
 to enable it via :ref:`a pragma directive<smt_checker>`.
 

docs/using-the-compiler.rst

@@ -372,6 +372,12 @@ Input Description
         {
           // Choose which model checker engine to use: all (default), bmc, chc, none.
           "engine": "chc",
+          // Choose which targets should be checked: all (default), constantCondition,
+          // underflow, overflow, divByZero, balance, assert, popEmptyArray.
+          // See the Formal Verification section for the targets description.
+          // Multiple targets can be selected at the same time, separated by a comma
+          // without spaces:
+          "targets": "underflow,overflow,assert",
           // Timeout for each SMT query in milliseconds.
           // If this option is not given, the SMTChecker will use a deterministic
           // resource limit by default.

libsolidity/CMakeLists.txt

@@ -102,6 +102,8 @@ set(sources
 	formal/EncodingContext.h
 	formal/ModelChecker.cpp
 	formal/ModelChecker.h
+	formal/ModelCheckerSettings.cpp
+	formal/ModelCheckerSettings.h
 	formal/Predicate.cpp
 	formal/Predicate.h
 	formal/PredicateInstance.cpp

libsolidity/formal/BMC.cpp

@@ -39,11 +39,12 @@ BMC::BMC(
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	smtutil::SMTSolverChoice _enabledSolvers,
-	optional<unsigned> _timeout
+	ModelCheckerSettings const& _settings
 ):
 	SMTEncoder(_context),
-	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _timeout)),
-	m_outerErrorReporter(_errorReporter)
+	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)),
+	m_outerErrorReporter(_errorReporter),
+	m_settings(_settings)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
 	if (_enabledSolvers.some())
@@ -58,7 +59,7 @@ BMC::BMC(
 #endif
 }
 
-void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTarget::Type>> _solvedTargets)
+void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
@@ -193,7 +194,7 @@ bool BMC::visit(IfStatement const& _node)
 	// specific input values.
 	if (isRootFunction())
 		addVerificationTarget(
-			VerificationTarget::Type::ConstantCondition,
+			VerificationTargetType::ConstantCondition,
 			expr(_node.condition()),
 			&_node.condition()
 		);
@@ -230,7 +231,7 @@ bool BMC::visit(Conditional const& _op)
 
 	if (isRootFunction())
 		addVerificationTarget(
-			VerificationTarget::Type::ConstantCondition,
+			VerificationTargetType::ConstantCondition,
 			expr(_op.condition()),
 			&_op.condition()
 		);
@@ -263,7 +264,7 @@ bool BMC::visit(WhileStatement const& _node)
 		_node.condition().accept(*this);
 		if (isRootFunction())
 			addVerificationTarget(
-				VerificationTarget::Type::ConstantCondition,
+				VerificationTargetType::ConstantCondition,
 				expr(_node.condition()),
 				&_node.condition()
 			);
@@ -273,7 +274,7 @@ bool BMC::visit(WhileStatement const& _node)
 		_node.condition().accept(*this);
 		if (isRootFunction())
 			addVerificationTarget(
-				VerificationTarget::Type::ConstantCondition,
+				VerificationTargetType::ConstantCondition,
 				expr(_node.condition()),
 				&_node.condition()
 			);
@@ -317,7 +318,7 @@ bool BMC::visit(ForStatement const& _node)
 		_node.condition()->accept(*this);
 		if (isRootFunction())
 			addVerificationTarget(
-				VerificationTarget::Type::ConstantCondition,
+				VerificationTargetType::ConstantCondition,
 				expr(*_node.condition()),
 				_node.condition()
 			);
@@ -392,7 +393,7 @@ void BMC::endVisit(UnaryOperation const& _op)
 
 	if (_op.getOperator() == Token::Sub && smt::isInteger(*_op.annotation().type))
 		addVerificationTarget(
-			VerificationTarget::Type::UnderOverflow,
+			VerificationTargetType::UnderOverflow,
 			expr(_op),
 			&_op
 		);
@@ -438,7 +439,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		smtutil::Expression thisBalance = m_context.state().balance();
 
 		addVerificationTarget(
-			VerificationTarget::Type::Balance,
+			VerificationTargetType::Balance,
 			thisBalance < expr(*value),
 			&_funCall
 		);
@@ -474,7 +475,7 @@ void BMC::visitAssert(FunctionCall const& _funCall)
 	solAssert(args.size() == 1, "");
 	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
 	addVerificationTarget(
-		VerificationTarget::Type::Assert,
+		VerificationTargetType::Assert,
 		expr(*args.front()),
 		&_funCall
 	);
@@ -487,7 +488,7 @@ void BMC::visitRequire(FunctionCall const& _funCall)
 	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
 	if (isRootFunction())
 		addVerificationTarget(
-			VerificationTarget::Type::ConstantCondition,
+			VerificationTargetType::ConstantCondition,
 			expr(*args.front()),
 			args.front().get()
 		);
@@ -497,7 +498,7 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.arguments().at(2), "");
 	addVerificationTarget(
-		VerificationTarget::Type::DivByZero,
+		VerificationTargetType::DivByZero,
 		expr(*_funCall.arguments().at(2)),
 		&_funCall
 	);
@@ -572,7 +573,7 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
 	// Unchecked does not disable div by 0 checks.
 	if (_op == Token::Div || _op == Token::Mod)
 		addVerificationTarget(
-			VerificationTarget::Type::DivByZero,
+			VerificationTargetType::DivByZero,
 			_right,
 			&_expression
 		);
@@ -590,24 +591,24 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
 	if (_op == Token::Mod)
 		return values;
 
-	VerificationTarget::Type type;
+	VerificationTargetType type;
 	// The order matters here:
 	// If _op is Div and intType is signed, we only care about overflow.
 	if (_op == Token::Div)
 	{
 		if (intType->isSigned())
 			// Signed division can only overflow.
-			type = VerificationTarget::Type::Overflow;
+			type = VerificationTargetType::Overflow;
 		else
 			// Unsigned division cannot underflow/overflow.
 			return values;
 	}
 	else if (intType->isSigned())
-		type = VerificationTarget::Type::UnderOverflow;
+		type = VerificationTargetType::UnderOverflow;
 	else if (_op == Token::Sub)
-		type = VerificationTarget::Type::Underflow;
+		type = VerificationTargetType::Underflow;
 	else if (_op == Token::Add || _op == Token::Mul)
-		type = VerificationTarget::Type::Overflow;
+		type = VerificationTargetType::Overflow;
 	else
 		solAssert(false, "");
 
@@ -674,26 +675,26 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
 {
 	switch (_target.type)
 	{
-		case VerificationTarget::Type::ConstantCondition:
+		case VerificationTargetType::ConstantCondition:
 			checkConstantCondition(_target);
 			break;
-		case VerificationTarget::Type::Underflow:
+		case VerificationTargetType::Underflow:
 			checkUnderflow(_target);
 			break;
-		case VerificationTarget::Type::Overflow:
+		case VerificationTargetType::Overflow:
 			checkOverflow(_target);
 			break;
-		case VerificationTarget::Type::UnderOverflow:
+		case VerificationTargetType::UnderOverflow:
 			checkUnderflow(_target);
 			checkOverflow(_target);
 			break;
-		case VerificationTarget::Type::DivByZero:
+		case VerificationTargetType::DivByZero:
 			checkDivByZero(_target);
 			break;
-		case VerificationTarget::Type::Balance:
+		case VerificationTargetType::Balance:
 			checkBalance(_target);
 			break;
-		case VerificationTarget::Type::Assert:
+		case VerificationTargetType::Assert:
 			checkAssert(_target);
 			break;
 		default:
@@ -714,15 +715,15 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target)
 void BMC::checkUnderflow(BMCVerificationTarget& _target)
 {
 	solAssert(
-		_target.type == VerificationTarget::Type::Underflow ||
-			_target.type == VerificationTarget::Type::UnderOverflow,
+		_target.type == VerificationTargetType::Underflow ||
+			_target.type == VerificationTargetType::UnderOverflow,
 		""
 	);
 
 	if (
 		m_solvedTargets.count(_target.expression) && (
-			m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::Underflow) ||
-			m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::UnderOverflow)
+			m_solvedTargets.at(_target.expression).count(VerificationTargetType::Underflow) ||
+			m_solvedTargets.at(_target.expression).count(VerificationTargetType::UnderOverflow)
 		)
 	)
 		return;
@@ -747,15 +748,15 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target)
 void BMC::checkOverflow(BMCVerificationTarget& _target)
 {
 	solAssert(
-		_target.type == VerificationTarget::Type::Overflow ||
-			_target.type == VerificationTarget::Type::UnderOverflow,
+		_target.type == VerificationTargetType::Overflow ||
+			_target.type == VerificationTargetType::UnderOverflow,
 		""
 	);
 
 	if (
 		m_solvedTargets.count(_target.expression) && (
-			m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::Overflow) ||
-			m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::UnderOverflow)
+			m_solvedTargets.at(_target.expression).count(VerificationTargetType::Overflow) ||
+			m_solvedTargets.at(_target.expression).count(VerificationTargetType::UnderOverflow)
 		)
 	)
 		return;
@@ -779,11 +780,11 @@ void BMC::checkOverflow(BMCVerificationTarget& _target)
 
 void BMC::checkDivByZero(BMCVerificationTarget& _target)
 {
-	solAssert(_target.type == VerificationTarget::Type::DivByZero, "");
+	solAssert(_target.type == VerificationTargetType::DivByZero, "");
 
 	if (
 		m_solvedTargets.count(_target.expression) &&
-		m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::DivByZero)
+		m_solvedTargets.at(_target.expression).count(VerificationTargetType::DivByZero)
 	)
 		return;
 
@@ -802,7 +803,7 @@ void BMC::checkDivByZero(BMCVerificationTarget& _target)
 
 void BMC::checkBalance(BMCVerificationTarget& _target)
 {
-	solAssert(_target.type == VerificationTarget::Type::Balance, "");
+	solAssert(_target.type == VerificationTargetType::Balance, "");
 	checkCondition(
 		_target.constraints && _target.value,
 		_target.callStack,
@@ -817,7 +818,7 @@ void BMC::checkBalance(BMCVerificationTarget& _target)
 
 void BMC::checkAssert(BMCVerificationTarget& _target)
 {
-	solAssert(_target.type == VerificationTarget::Type::Assert, "");
+	solAssert(_target.type == VerificationTargetType::Assert, "");
 
 	if (
 		m_solvedTargets.count(_target.expression) &&
@@ -837,11 +838,14 @@ void BMC::checkAssert(BMCVerificationTarget& _target)
 }
 
 void BMC::addVerificationTarget(
-	VerificationTarget::Type _type,
+	VerificationTargetType _type,
 	smtutil::Expression const& _value,
 	Expression const* _expression
 )
 {
+	if (!m_settings.targets.has(_type))
+		return;
+
 	BMCVerificationTarget target{
 		{
 			_type,
@@ -852,7 +856,7 @@ void BMC::addVerificationTarget(
 		m_callStack,
 		modelExpressions()
 	};
-	if (_type == VerificationTarget::Type::ConstantCondition)
+	if (_type == VerificationTargetType::ConstantCondition)
 		checkVerificationTarget(target);
 	else
 		m_verificationTargets.emplace_back(move(target));

libsolidity/formal/BMC.h

@@ -30,6 +30,7 @@
 
 
 #include <libsolidity/formal/EncodingContext.h>
+#include <libsolidity/formal/ModelCheckerSettings.h>
 #include <libsolidity/formal/SMTEncoder.h>
 
 #include <libsolidity/interface/ReadFile.h>
@@ -62,10 +63,10 @@ public:
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		smtutil::SMTSolverChoice _enabledSolvers,
-		std::optional<unsigned> timeout
+		ModelCheckerSettings const& _settings
 	);
 
-	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTarget::Type>> _solvedTargets);
+	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>> _solvedTargets);
 
 	/// This is used if the SMT solver is not directly linked into this binary.
 	/// @returns a list of inputs to the SMT solver that were not part of the argument to
@@ -140,7 +141,7 @@ private:
 	void checkBalance(BMCVerificationTarget& _target);
 	void checkAssert(BMCVerificationTarget& _target);
 	void addVerificationTarget(
-		VerificationTarget::Type _type,
+		VerificationTargetType _type,
 		smtutil::Expression const& _value,
 		Expression const* _expression
 	);
@@ -186,7 +187,9 @@ private:
 	std::vector<BMCVerificationTarget> m_verificationTargets;
 
 	/// Targets that were already proven.
-	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_solvedTargets;
+	std::map<ASTNode const*, std::set<VerificationTargetType>> m_solvedTargets;
+
+	ModelCheckerSettings const& m_settings;
 };
 
 }

libsolidity/formal/CHC.cpp

@@ -54,12 +54,12 @@ CHC::CHC(
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
 	SMTSolverChoice _enabledSolvers,
-	optional<unsigned> _timeout
+	ModelCheckerSettings const& _settings
 ):
 	SMTEncoder(_context),
 	m_outerErrorReporter(_errorReporter),
 	m_enabledSolvers(_enabledSolvers),
-	m_queryTimeout(_timeout)
+	m_settings(_settings)
 {
 	bool usesZ3 = _enabledSolvers.z3;
 #ifdef HAVE_Z3
@@ -68,7 +68,7 @@ CHC::CHC(
 	usesZ3 = false;
 #endif
 	if (!usesZ3)
-		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_queryTimeout);
+		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_settings.timeout);
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -606,14 +606,14 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	solAssert(m_currentContract, "");
 	solAssert(m_currentFunction, "");
 	auto errorCondition = !m_context.expression(*args.front())->currentValue();
-	verificationTargetEncountered(&_funCall, VerificationTarget::Type::Assert, errorCondition);
+	verificationTargetEncountered(&_funCall, VerificationTargetType::Assert, errorCondition);
 }
 
 void CHC::visitAddMulMod(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.arguments().at(2), "");
 
-	verificationTargetEncountered(&_funCall, VerificationTarget::Type::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
+	verificationTargetEncountered(&_funCall, VerificationTargetType::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
 
 	SMTEncoder::visitAddMulMod(_funCall);
 }
@@ -773,7 +773,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
 
-	verificationTargetEncountered(&_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0);
+	verificationTargetEncountered(&_arrayPop, VerificationTargetType::PopEmptyArray, symbArray->length() <= 0);
 }
 
 pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
@@ -786,7 +786,7 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 {
 	// Unchecked does not disable div by 0 checks.
 	if (_op == Token::Mod || _op == Token::Div)
-		verificationTargetEncountered(&_expression, VerificationTarget::Type::DivByZero, _right == 0);
+		verificationTargetEncountered(&_expression, VerificationTargetType::DivByZero, _right == 0);
 
 	auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
 
@@ -805,16 +805,16 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 		return values;
 
 	if (_op == Token::Div)
-		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTargetType::Overflow, values.second > intType->maxValue());
 	else if (intType->isSigned())
 	{
-		verificationTargetEncountered(&_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
-		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTargetType::Underflow, values.second < intType->minValue());
+		verificationTargetEncountered(&_expression, VerificationTargetType::Overflow, values.second > intType->maxValue());
 	}
 	else if (_op == Token::Sub)
-		verificationTargetEncountered(&_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
+		verificationTargetEncountered(&_expression, VerificationTargetType::Underflow, values.second < intType->minValue());
 	else if (_op == Token::Add || _op == Token::Mul)
-		verificationTargetEncountered(&_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
+		verificationTargetEncountered(&_expression, VerificationTargetType::Overflow, values.second > intType->maxValue());
 	else
 		solAssert(false, "");
 	return values;
@@ -843,7 +843,7 @@ void CHC::resetSourceAnalysis()
 	if (usesZ3)
 	{
 		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
-		m_interface.reset(new Z3CHCInterface(m_queryTimeout));
+		m_interface.reset(new Z3CHCInterface(m_settings.timeout));
 		auto z3Interface = dynamic_cast<Z3CHCInterface const*>(m_interface.get());
 		solAssert(z3Interface, "");
 		m_context.setSolver(z3Interface->z3Interface());
@@ -1324,10 +1324,14 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
 
 void CHC::verificationTargetEncountered(
 	ASTNode const* const _errorNode,
-	VerificationTarget::Type _type,
+	VerificationTargetType _type,
 	smtutil::Expression const& _errorCondition
 )
 {
+
+	if (!m_settings.targets.has(_type))
+		return;
+
 	solAssert(m_currentContract || m_currentFunction, "");
 	SourceUnit const* source = m_currentContract ? sourceUnitContaining(*m_currentContract) : sourceUnitContaining(*m_currentFunction);
 	solAssert(source, "");
@@ -1384,15 +1388,15 @@ void CHC::checkVerificationTargets()
 		string errorType;
 		ErrorId errorReporterId;
 
-		if (target.type == VerificationTarget::Type::PopEmptyArray)
+		if (target.type == VerificationTargetType::PopEmptyArray)
 		{
 			solAssert(dynamic_cast<FunctionCall const*>(target.errorNode), "");
 			errorType = "Empty array \"pop\"";
 			errorReporterId = 2529_error;
 		}
 		else if (
-			target.type == VerificationTarget::Type::Underflow ||
-			target.type == VerificationTarget::Type::Overflow
+			target.type == VerificationTargetType::Underflow ||
+			target.type == VerificationTargetType::Overflow
 		)
 		{
 			auto const* expr = dynamic_cast<Expression const*>(target.errorNode);
@@ -1401,23 +1405,23 @@ void CHC::checkVerificationTargets()
 			if (!intType)
 				intType = TypeProvider::uint256();
 
-			if (target.type == VerificationTarget::Type::Underflow)
+			if (target.type == VerificationTargetType::Underflow)
 			{
 				errorType = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
 				errorReporterId = 3944_error;
 			}
-			else if (target.type == VerificationTarget::Type::Overflow)
+			else if (target.type == VerificationTargetType::Overflow)
 			{
 				errorType = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
 				errorReporterId = 4984_error;
 			}
 		}
-		else if (target.type == VerificationTarget::Type::DivByZero)
+		else if (target.type == VerificationTargetType::DivByZero)
 		{
 			errorType = "Division by zero";
 			errorReporterId = 4281_error;
 		}
-		else if (target.type == VerificationTarget::Type::Assert)
+		else if (target.type == VerificationTargetType::Assert)
 		{
 			errorType = "Assertion violation";
 			errorReporterId = 6328_error;

libsolidity/formal/CHC.h

@@ -31,6 +31,7 @@
 
 #pragma once
 
+#include <libsolidity/formal/ModelCheckerSettings.h>
 #include <libsolidity/formal/Predicate.h>
 #include <libsolidity/formal/SMTEncoder.h>
 
@@ -56,13 +57,13 @@ public:
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		smtutil::SMTSolverChoice _enabledSolvers,
-		std::optional<unsigned> timeout
+		ModelCheckerSettings const& _settings
 	);
 
 	void analyze(SourceUnit const& _sources);
 
-	std::map<ASTNode const*, std::set<VerificationTarget::Type>> const& safeTargets() const { return m_safeTargets; }
-	std::map<ASTNode const*, std::set<VerificationTarget::Type>> const& unsafeTargets() const { return m_unsafeTargets; }
+	std::map<ASTNode const*, std::set<VerificationTargetType>> const& safeTargets() const { return m_safeTargets; }
+	std::map<ASTNode const*, std::set<VerificationTargetType>> const& unsafeTargets() const { return m_unsafeTargets; }
 
 	/// This is used if the Horn solver is not directly linked into this binary.
 	/// @returns a list of inputs to the Horn solver that were not part of the argument to
@@ -199,7 +200,7 @@ private:
 	/// @returns <false, model> otherwise.
 	std::pair<smtutil::CheckResult, smtutil::CHCSolverInterface::CexGraph> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
 
-	void verificationTargetEncountered(ASTNode const* const _errorNode, VerificationTarget::Type _type, smtutil::Expression const& _errorCondition);
+	void verificationTargetEncountered(ASTNode const* const _errorNode, VerificationTargetType _type, smtutil::Expression const& _errorCondition);
 
 	void checkVerificationTargets();
 	// Forward declaration. Definition is below.
@@ -321,9 +322,9 @@ private:
 	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
 	/// Targets proven safe.
-	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_safeTargets;
+	std::map<ASTNode const*, std::set<VerificationTargetType>> m_safeTargets;
 	/// Targets proven unsafe.
-	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_unsafeTargets;
+	std::map<ASTNode const*, std::set<VerificationTargetType>> m_unsafeTargets;
 	//@}
 
 	/// Control-flow.
@@ -369,8 +370,7 @@ private:
 	/// SMT solvers that are chosen at runtime.
 	smtutil::SMTSolverChoice m_enabledSolvers;
 
-	/// SMT query timeout in seconds.
-	std::optional<unsigned> m_queryTimeout;
+	ModelCheckerSettings const& m_settings;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -36,8 +36,8 @@ ModelChecker::ModelChecker(
 ):
 	m_settings(_settings),
 	m_context(),
-	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)
+	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings),
+	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings)
 {
 }
 

libsolidity/formal/ModelChecker.h

@@ -26,14 +26,13 @@
 #include <libsolidity/formal/BMC.h>
 #include <libsolidity/formal/CHC.h>
 #include <libsolidity/formal/EncodingContext.h>
+#include <libsolidity/formal/ModelCheckerSettings.h>
 
 #include <libsolidity/interface/ReadFile.h>
 
 #include <libsmtutil/SolverInterface.h>
 #include <liblangutil/ErrorReporter.h>
 
-#include <optional>
-
 namespace solidity::langutil
 {
 class ErrorReporter;
@@ -43,40 +42,6 @@ struct SourceLocation;
 namespace solidity::frontend
 {
 
-struct ModelCheckerEngine
-{
-	bool bmc = false;
-	bool chc = false;
-
-	static constexpr ModelCheckerEngine All() { return {true, true}; }
-	static constexpr ModelCheckerEngine BMC() { return {true, false}; }
-	static constexpr ModelCheckerEngine CHC() { return {false, true}; }
-	static constexpr ModelCheckerEngine None() { return {false, false}; }
-
-	bool none() const { return !any(); }
-	bool any() const { return bmc || chc; }
-	bool all() const { return bmc && chc; }
-
-	static std::optional<ModelCheckerEngine> fromString(std::string const& _engine)
-	{
-		static std::map<std::string, ModelCheckerEngine> engineMap{
-			{"all", All()},
-			{"bmc", BMC()},
-			{"chc", CHC()},
-			{"none", None()}
-		};
-		if (engineMap.count(_engine))
-			return engineMap.at(_engine);
-		return {};
-	}
-};
-
-struct ModelCheckerSettings
-{
-	ModelCheckerEngine engine = ModelCheckerEngine::All();
-	std::optional<unsigned> timeout;
-};
-
 class ModelChecker
 {
 public:

libsolidity/formal/ModelCheckerSettings.cpp

@@ -0,0 +1,55 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/ModelCheckerSettings.h>
+
+#include <optional>
+#include <range/v3/view.hpp>
+
+using namespace std;
+using namespace ranges;
+using namespace solidity;
+using namespace solidity::frontend;
+
+std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
+{
+	using TargetType = VerificationTargetType;
+	static map<string, TargetType> const targetStrings{
+		{"constantCondition", TargetType::ConstantCondition},
+		{"underflow", TargetType::Underflow},
+		{"overflow", TargetType::Overflow},
+		{"divByZero", TargetType::DivByZero},
+		{"balance", TargetType::Balance},
+		{"assert", TargetType::Assert},
+		{"popEmptyArray", TargetType::PopEmptyArray}
+	};
+
+	set<TargetType> chosenTargets;
+	if (_targets == "all")
+		for (auto&& v: targetStrings | views::values)
+			chosenTargets.insert(v);
+	else
+		for (auto&& t: _targets | views::split(',') | ranges::to<vector<string>>())
+		{
+			if (!targetStrings.count(t))
+				return {};
+			chosenTargets.insert(targetStrings.at(t));
+		}
+
+	return ModelCheckerTargets{chosenTargets};
+}

libsolidity/formal/ModelCheckerSettings.h

@@ -0,0 +1,77 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsmtutil/SolverInterface.h>
+
+#include <optional>
+#include <set>
+
+namespace solidity::frontend
+{
+
+struct ModelCheckerEngine
+{
+	bool bmc = false;
+	bool chc = false;
+
+	static constexpr ModelCheckerEngine All() { return {true, true}; }
+	static constexpr ModelCheckerEngine BMC() { return {true, false}; }
+	static constexpr ModelCheckerEngine CHC() { return {false, true}; }
+	static constexpr ModelCheckerEngine None() { return {false, false}; }
+
+	bool none() const { return !any(); }
+	bool any() const { return bmc || chc; }
+	bool all() const { return bmc && chc; }
+
+	static std::optional<ModelCheckerEngine> fromString(std::string const& _engine)
+	{
+		static std::map<std::string, ModelCheckerEngine> engineMap{
+			{"all", All()},
+			{"bmc", BMC()},
+			{"chc", CHC()},
+			{"none", None()}
+		};
+		if (engineMap.count(_engine))
+			return engineMap.at(_engine);
+		return {};
+	}
+};
+
+enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray };
+
+struct ModelCheckerTargets
+{
+	static ModelCheckerTargets All() { return *fromString("all"); }
+	static ModelCheckerTargets None() { return {}; }
+
+	static std::optional<ModelCheckerTargets> fromString(std::string const& _targets);
+
+	bool has(VerificationTargetType _type) const { return targets.count(_type); }
+	std::set<VerificationTargetType> targets;
+};
+
+struct ModelCheckerSettings
+{
+	ModelCheckerEngine engine = ModelCheckerEngine::All();
+	ModelCheckerTargets targets = ModelCheckerTargets::All();
+	std::optional<unsigned> timeout;
+};
+
+}

libsolidity/formal/SMTEncoder.h

@@ -25,6 +25,7 @@
 
 
 #include <libsolidity/formal/EncodingContext.h>
+#include <libsolidity/formal/ModelCheckerSettings.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 #include <libsolidity/formal/VariableUsage.h>
 
@@ -348,7 +349,7 @@ protected:
 
 	struct VerificationTarget
 	{
-		enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray } type;
+		VerificationTargetType type;
 		smtutil::Expression value;
 		smtutil::Expression constraints;
 	};

libsolidity/interface/CompilerStack.h

@@ -29,7 +29,7 @@
 #include <libsolidity/interface/Version.h>
 #include <libsolidity/interface/DebugSettings.h>
 
-#include <libsolidity/formal/ModelChecker.h>
+#include <libsolidity/formal/ModelCheckerSettings.h>
 
 #include <libsmtutil/SolverInterface.h>
 

libsolidity/interface/StandardCompiler.cpp

@@ -434,7 +434,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"engine", "timeout"};
+	static set<string> keys{"engine", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -908,6 +908,16 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.engine = *engine;
 	}
 
+	if (modelCheckerSettings.isMember("targets"))
+	{
+		if (!modelCheckerSettings["targets"].isString())
+			return formatFatalError("JSONError", "settings.modelChecker.targets must be a string.");
+		std::optional<ModelCheckerTargets> targets = ModelCheckerTargets::fromString(modelCheckerSettings["targets"].asString());
+		if (!targets)
+			return formatFatalError("JSONError", "Invalid model checker targets requested.");
+		ret.modelCheckerSettings.targets = *targets;
+	}
+
 	if (modelCheckerSettings.isMember("timeout"))
 	{
 		if (!modelCheckerSettings["timeout"].isUInt())

solc/CommandLineInterface.cpp

@@ -153,6 +153,7 @@ static string const g_strMetadata = "metadata";
 static string const g_strMetadataHash = "metadata-hash";
 static string const g_strMetadataLiteral = "metadata-literal";
 static string const g_strModelCheckerEngine = "model-checker-engine";
+static string const g_strModelCheckerTargets = "model-checker-targets";
 static string const g_strModelCheckerTimeout = "model-checker-timeout";
 static string const g_strNatspecDev = "devdoc";
 static string const g_strNatspecUser = "userdoc";
@@ -224,6 +225,7 @@ static string const g_argMetadata = g_strMetadata;
 static string const g_argMetadataHash = g_strMetadataHash;
 static string const g_argMetadataLiteral = g_strMetadataLiteral;
 static string const g_argModelCheckerEngine = g_strModelCheckerEngine;
+static string const g_argModelCheckerTargets = g_strModelCheckerTargets;
 static string const g_argModelCheckerTimeout = g_strModelCheckerTimeout;
 static string const g_argNatspecDev = g_strNatspecDev;
 static string const g_argNatspecUser = g_strNatspecUser;
@@ -1033,6 +1035,13 @@ General Information)").c_str(),
 			po::value<string>()->value_name("all,bmc,chc,none")->default_value("all"),
 			"Select model checker engine."
 		)
+		(
+			g_strModelCheckerTargets.c_str(),
+			po::value<string>()->value_name("all,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray")->default_value("all"),
+			"Select model checker verification targets. "
+			"Multiple targets can be selected at the same time, separated by a comma "
+			"and no spaces."
+		)
 		(
 			g_strModelCheckerTimeout.c_str(),
 			po::value<unsigned>()->value_name("ms"),
@@ -1452,6 +1461,18 @@ bool CommandLineInterface::processInput()
 		m_modelCheckerSettings.engine = *engine;
 	}
 
+	if (m_args.count(g_argModelCheckerTargets))
+	{
+		string targetsStr = m_args[g_argModelCheckerTargets].as<string>();
+		optional<ModelCheckerTargets> targets = ModelCheckerTargets::fromString(targetsStr);
+		if (!targets)
+		{
+			serr() << "Invalid option for --" << g_argModelCheckerTargets << ": " << targetsStr << endl;
+			return false;
+		}
+		m_modelCheckerSettings.targets = *targets;
+	}
+
 	if (m_args.count(g_argModelCheckerTimeout))
 		m_modelCheckerSettings.timeout = m_args[g_argModelCheckerTimeout].as<unsigned>();
 

test/cmdlineTests/model_checker_targets_all/args

@@ -0,0 +1 @@
+--model-checker-targets all

test/cmdlineTests/model_checker_targets_all/err

@@ -0,0 +1,93 @@
+Warning: CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)
+ --> model_checker_targets_all/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^
+
+Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)
+ --> model_checker_targets_all/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^
+
+Warning: CHC: Division by zero happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_all/input.sol:10:3:
+   |
+10 | 		2 / x;
+   | 		^^^^^
+
+Warning: CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_all/input.sol:12:3:
+   |
+12 | 		assert(x > 0);
+   | 		^^^^^^^^^^^^^
+
+Warning: CHC: Empty array "pop" happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_all/input.sol:13:3:
+   |
+13 | 		arr.pop();
+   | 		^^^^^^^^^
+
+Warning: BMC: Condition is always true.
+ --> model_checker_targets_all/input.sol:7:11:
+  |
+7 | 		require(x >= 0);
+  | 		        ^^^^^^
+Note: Callstack:
+
+Warning: BMC: Insufficient funds happens here.
+  --> model_checker_targets_all/input.sol:11:3:
+   |
+11 | 		a.transfer(x);
+   | 		^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_all/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_all_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets all

test/cmdlineTests/model_checker_targets_all_bmc/err

@@ -0,0 +1,69 @@
+Warning: BMC: Condition is always true.
+ --> model_checker_targets_all_bmc/input.sol:7:11:
+  |
+7 | 		require(x >= 0);
+  | 		        ^^^^^^
+Note: Callstack:
+
+Warning: BMC: Underflow (resulting value less than 0) happens here.
+ --> model_checker_targets_all_bmc/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^
+Note: Counterexample:
+  <result> = (- 1)
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+ --> model_checker_targets_all_bmc/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^
+Note: Counterexample:
+  <result> = 2**256
+  a = 0
+  x = 1
+
+Note: Callstack:
+Note:
+
+Warning: BMC: Division by zero happens here.
+  --> model_checker_targets_all_bmc/input.sol:10:3:
+   |
+10 | 		2 / x;
+   | 		^^^^^
+Note: Counterexample:
+  <result> = 0
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+Warning: BMC: Insufficient funds happens here.
+  --> model_checker_targets_all_bmc/input.sol:11:3:
+   |
+11 | 		a.transfer(x);
+   | 		^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+Warning: BMC: Assertion violation happens here.
+  --> model_checker_targets_all_bmc/input.sol:12:3:
+   |
+12 | 		assert(x > 0);
+   | 		^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_all_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_all_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets all

test/cmdlineTests/model_checker_targets_all_chc/err

@@ -0,0 +1,74 @@
+Warning: CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)
+ --> model_checker_targets_all_chc/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^
+
+Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)
+ --> model_checker_targets_all_chc/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^
+
+Warning: CHC: Division by zero happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_all_chc/input.sol:10:3:
+   |
+10 | 		2 / x;
+   | 		^^^^^
+
+Warning: CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_all_chc/input.sol:12:3:
+   |
+12 | 		assert(x > 0);
+   | 		^^^^^^^^^^^^^
+
+Warning: CHC: Empty array "pop" happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_all_chc/input.sol:13:3:
+   |
+13 | 		arr.pop();
+   | 		^^^^^^^^^

test/cmdlineTests/model_checker_targets_all_chc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_assert_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets assert

test/cmdlineTests/model_checker_targets_assert_bmc/err

@@ -0,0 +1,11 @@
+Warning: BMC: Assertion violation happens here.
+  --> model_checker_targets_assert_bmc/input.sol:12:3:
+   |
+12 | 		assert(x > 0);
+   | 		^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_assert_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_assert_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets assert

test/cmdlineTests/model_checker_targets_assert_chc/err

@@ -0,0 +1,14 @@
+Warning: CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_assert_chc/input.sol:12:3:
+   |
+12 | 		assert(x > 0);
+   | 		^^^^^^^^^^^^^

test/cmdlineTests/model_checker_targets_assert_chc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_balance_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets balance

test/cmdlineTests/model_checker_targets_balance_bmc/err

@@ -0,0 +1,11 @@
+Warning: BMC: Insufficient funds happens here.
+  --> model_checker_targets_balance_bmc/input.sol:11:3:
+   |
+11 | 		a.transfer(x);
+   | 		^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_balance_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_balance_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets balance

test/cmdlineTests/model_checker_targets_balance_chc/err

@@ -0,0 +1,2 @@
+Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
+--> model_checker_targets_balance_chc/input.sol

test/cmdlineTests/model_checker_targets_balance_chc/input.sol

@@ -0,0 +1,14 @@
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_constant_condition_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets constantCondition

test/cmdlineTests/model_checker_targets_constant_condition_bmc/err

@@ -0,0 +1,6 @@
+Warning: BMC: Condition is always true.
+ --> model_checker_targets_constant_condition_bmc/input.sol:7:11:
+  |
+7 | 		require(x >= 0);
+  | 		        ^^^^^^
+Note: Callstack:

test/cmdlineTests/model_checker_targets_constant_condition_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_constant_condition_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets constantCondition

test/cmdlineTests/model_checker_targets_constant_condition_chc/err

@@ -0,0 +1,2 @@
+Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
+--> model_checker_targets_constant_condition_chc/input.sol

test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol

@@ -0,0 +1,14 @@
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_div_by_zero_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets divByZero

test/cmdlineTests/model_checker_targets_div_by_zero_bmc/err

@@ -0,0 +1,12 @@
+Warning: BMC: Division by zero happens here.
+  --> model_checker_targets_div_by_zero_bmc/input.sol:10:3:
+   |
+10 | 		2 / x;
+   | 		^^^^^
+Note: Counterexample:
+  <result> = 0
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_div_by_zero_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_div_by_zero_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets divByZero

test/cmdlineTests/model_checker_targets_div_by_zero_chc/err

@@ -0,0 +1,14 @@
+Warning: CHC: Division by zero happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_div_by_zero_chc/input.sol:10:3:
+   |
+10 | 		2 / x;
+   | 		^^^^^

test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_error/args

@@ -0,0 +1 @@
+--model-checker-targets aaa,bbb

test/cmdlineTests/model_checker_targets_error/err

@@ -0,0 +1 @@
+Invalid option for --model-checker-targets: aaa,bbb

test/cmdlineTests/model_checker_targets_error/exit

@@ -0,0 +1 @@
+1

test/cmdlineTests/model_checker_targets_error/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_overflow_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets overflow

test/cmdlineTests/model_checker_targets_overflow_bmc/err

@@ -0,0 +1,12 @@
+Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+ --> model_checker_targets_overflow_bmc/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^
+Note: Counterexample:
+  <result> = 2**256
+  a = 0
+  x = 1
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_overflow_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_overflow_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets overflow

test/cmdlineTests/model_checker_targets_overflow_chc/err

@@ -0,0 +1,14 @@
+Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)
+ --> model_checker_targets_overflow_chc/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^

test/cmdlineTests/model_checker_targets_overflow_chc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_pop_empty_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets popEmptyArray

test/cmdlineTests/model_checker_targets_pop_empty_bmc/err

@@ -0,0 +1,2 @@
+Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
+--> model_checker_targets_pop_empty_bmc/input.sol

test/cmdlineTests/model_checker_targets_pop_empty_bmc/input.sol

@@ -0,0 +1,14 @@
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_pop_empty_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets popEmptyArray

test/cmdlineTests/model_checker_targets_pop_empty_chc/err

@@ -0,0 +1,14 @@
+Warning: CHC: Empty array "pop" happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_pop_empty_chc/input.sol:13:3:
+   |
+13 | 		arr.pop();
+   | 		^^^^^^^^^

test/cmdlineTests/model_checker_targets_pop_empty_chc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_underflow_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets underflow

test/cmdlineTests/model_checker_targets_underflow_bmc/err

@@ -0,0 +1,12 @@
+Warning: BMC: Underflow (resulting value less than 0) happens here.
+ --> model_checker_targets_underflow_bmc/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^
+Note: Counterexample:
+  <result> = (- 1)
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_underflow_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_underflow_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets underflow

test/cmdlineTests/model_checker_targets_underflow_chc/err

@@ -0,0 +1,14 @@
+Warning: CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)
+ --> model_checker_targets_underflow_chc/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^

test/cmdlineTests/model_checker_targets_underflow_chc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_underflow_overflow_assert_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets underflow,overflow,assert

test/cmdlineTests/model_checker_targets_underflow_overflow_assert_bmc/err

@@ -0,0 +1,37 @@
+Warning: BMC: Underflow (resulting value less than 0) happens here.
+ --> model_checker_targets_underflow_overflow_assert_bmc/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^
+Note: Counterexample:
+  <result> = (- 1)
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+ --> model_checker_targets_underflow_overflow_assert_bmc/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^
+Note: Counterexample:
+  <result> = 2**256
+  a = 0
+  x = 1
+
+Note: Callstack:
+Note:
+
+Warning: BMC: Assertion violation happens here.
+  --> model_checker_targets_underflow_overflow_assert_bmc/input.sol:12:3:
+   |
+12 | 		assert(x > 0);
+   | 		^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_underflow_overflow_assert_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets underflow,overflow,assert

test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err

@@ -0,0 +1,44 @@
+Warning: CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)
+ --> model_checker_targets_underflow_overflow_assert_chc/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^
+
+Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)
+ --> model_checker_targets_underflow_overflow_assert_chc/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^
+
+Warning: CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> model_checker_targets_underflow_overflow_assert_chc/input.sol:12:3:
+   |
+12 | 		assert(x > 0);
+   | 		^^^^^^^^^^^^^

test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_underflow_overflow_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-targets underflow,overflow

test/cmdlineTests/model_checker_targets_underflow_overflow_bmc/err

@@ -0,0 +1,25 @@
+Warning: BMC: Underflow (resulting value less than 0) happens here.
+ --> model_checker_targets_underflow_overflow_bmc/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^
+Note: Counterexample:
+  <result> = (- 1)
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+ --> model_checker_targets_underflow_overflow_bmc/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^
+Note: Counterexample:
+  <result> = 2**256
+  a = 0
+  x = 1
+
+Note: Callstack:
+Note:

test/cmdlineTests/model_checker_targets_underflow_overflow_bmc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/model_checker_targets_underflow_overflow_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-targets underflow,overflow

test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err

@@ -0,0 +1,29 @@
+Warning: CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)
+ --> model_checker_targets_underflow_overflow_chc/input.sol:8:3:
+  |
+8 | 		--x;
+  | 		^^^
+
+Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)
+ --> model_checker_targets_underflow_overflow_chc/input.sol:9:3:
+  |
+9 | 		x + type(uint).max;
+  | 		^^^^^^^^^^^^^^^^^^

test/cmdlineTests/model_checker_targets_underflow_overflow_chc/input.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+pragma experimental SMTChecker;
+contract test {
+	uint[] arr;
+    function f(address payable a, uint x) public {
+		require(x >= 0);
+		--x;
+		x + type(uint).max;
+		2 / x;
+		a.transfer(x);
+		assert(x > 0);
+		arr.pop();
+    }
+}

test/cmdlineTests/standard_model_checker_targets_all/input.json

@@ -0,0 +1,28 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"targets": "all"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_all/output.json

@@ -0,0 +1,247 @@
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x35cba50832f92f2e4e2c62c810158291d12ee4cb303a48798b61fa8c7945d055":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) (not expr_15_1)))
+(check-sat)
+","0x5832e3dd270bc6310bad32552048faf832f79805e01d061abf4da38d57cf5be2":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_1| () Int)
+(declare-fun |x_9_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_26_1| () Int)
+(declare-fun |expr_27_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_0| () Int)
+(declare-fun |d_div_mod_12_0| () Int)
+(declare-fun |r_div_mod_12_0| () Int)
+(declare-fun |expr_31_1| () Int)
+(declare-fun |expr_33_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |state_1| () |state_type|)
+(declare-fun |state_2| () |state_type|)
+(declare-fun |state_3| () |state_type|)
+(declare-fun |expr_40_0| () Int)
+(declare-fun |expr_41_0| () Int)
+(declare-fun |expr_42_1| () Bool)
+(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
+(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
+
+(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) true) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_12_0)) (and (and (<= 0 r_div_mod_12_0) (or (= expr_30_0 0) (< r_div_mod_12_0 expr_30_0))) (and (= (+ (* d_div_mod_12_0 expr_30_0) r_div_mod_12_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| a_7_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| x_9_1))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
+","0xad522252173a6aa6ab3a770ff3f11427f810c4f5db7e6e5f639c8a21962b28f5":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) expr_15_1))
+(check-sat)
+"}},"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)
+ --> A:8:7:
+  |
+8 | \t\t\t\t\t\t--x;
+  | \t\t\t\t\t\t^^^
+
+","message":"CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)","severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)
+ --> A:9:7:
+  |
+9 | \t\t\t\t\t\tx + type(uint).max;
+  | \t\t\t\t\t\t^^^^^^^^^^^^^^^^^^
+
+","message":"CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)","severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> A:10:7:
+   |
+10 | \t\t\t\t\t\t2 / x;
+   | \t\t\t\t\t\t^^^^^
+
+","message":"CHC: Division by zero happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)","severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> A:12:7:
+   |
+12 | \t\t\t\t\t\tassert(x > 0);
+   | \t\t\t\t\t\t^^^^^^^^^^^^^
+
+","message":"CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> A:13:7:
+   |
+13 | \t\t\t\t\t\tarr.pop();
+   | \t\t\t\t\t\t^^^^^^^^^
+
+","message":"CHC: Empty array \"pop\" happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
+ --> A:7:15:
+  |
+7 | \t\t\t\t\t\trequire(x >= 0);
+  | \t\t\t\t\t\t        ^^^^^^
+Note: Callstack:
+
+","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":196,"file":"A","start":190},"type":"Warning"},{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
+  --> A:11:7:
+   |
+11 | \t\t\t\t\t\ta.transfer(x);
+   | \t\t\t\t\t\t^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
+  a = 0
+  x = 0
+"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":268,"file":"A","start":255},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json

@@ -0,0 +1,29 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "bmc",
+			"targets": "all"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_all_bmc/output.json

@@ -0,0 +1,415 @@
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x0a6e9ee4fe334d65b2abe8c35c92729ad3012940f546f260167f1d47d3746bd9":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_1| () Int)
+(declare-fun |x_9_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_26_1| () Int)
+(declare-fun |expr_27_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_31_1| () Int)
+(declare-fun |expr_33_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |state_1| () |state_type|)
+(declare-fun |state_2| () |state_type|)
+(declare-fun |state_3| () |state_type|)
+(declare-fun |expr_40_0| () Int)
+(declare-fun |expr_41_0| () Int)
+(declare-fun |expr_42_1| () Bool)
+(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
+(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
+
+(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) true) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| a_7_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| x_9_1))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
+","0x35cba50832f92f2e4e2c62c810158291d12ee4cb303a48798b61fa8c7945d055":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) (not expr_15_1)))
+(check-sat)
+","0xa11872d9caace0479351e125d6feeb0d28b2b5e28bca4eb8b19c0139c4f94594":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_1| () Int)
+(declare-fun |x_9_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_26_1| () Int)
+(declare-fun |expr_27_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_31_1| () Int)
+(declare-fun |expr_33_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |state_1| () |state_type|)
+(declare-fun |state_2| () |state_type|)
+(declare-fun |state_3| () |state_type|)
+(declare-fun |expr_40_0| () Int)
+(declare-fun |expr_41_0| () Int)
+(declare-fun |expr_42_1| () Bool)
+(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
+(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
+
+(assert (and (and (and true true) (and (= expr_42_1 (> expr_40_0 expr_41_0)) (and (implies (and true true) true) (and (= expr_41_0 0) (and (implies (and true true) (and (>= expr_40_0 0) (<= expr_40_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_40_0 x_9_1) (and (= state_3 (ite (= this_0 expr_33_0) state_0 state_2)) (and (= state_2 (|state_type| (store (|balances| state_1) expr_33_0 (+ (select (|balances| state_1) expr_33_0) expr_36_0)))) (and (= state_1 (|state_type| (store (|balances| state_0) this_0 (+ (select (|balances| state_0) this_0) (- 0 expr_36_0))))) (and (and (>= (select (|balances| state_0) this_0) 0) (<= (select (|balances| state_0) this_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) true) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true))))))))))))))))))))))))))))))))))))))))))) (not expr_42_1)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| a_7_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| x_9_1))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
+","0xad522252173a6aa6ab3a770ff3f11427f810c4f5db7e6e5f639c8a21962b28f5":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) expr_15_1))
+(check-sat)
+","0xbff03f53a7de50d2b79369639ee478ab1b8df545104dc83d93aafae02dde855a":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_1| () Int)
+(declare-fun |x_9_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_26_1| () Int)
+(declare-fun |expr_27_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_31_1| () Int)
+(declare-fun |expr_33_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |state_1| () |state_type|)
+(declare-fun |state_2| () |state_type|)
+(declare-fun |state_3| () |state_type|)
+(declare-fun |expr_40_0| () Int)
+(declare-fun |expr_41_0| () Int)
+(declare-fun |expr_42_1| () Bool)
+(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
+(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
+
+(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true))))))))))))) (< (- x_9_0 1) 0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| a_7_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| x_9_0))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| (- x_9_0 1)))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
+","0xc23473f0d9042c91db2816923860cf271ed38d055bf0c0a61ef777a2d890a4a3":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_1| () Int)
+(declare-fun |x_9_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_26_1| () Int)
+(declare-fun |expr_27_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_31_1| () Int)
+(declare-fun |expr_33_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |state_1| () |state_type|)
+(declare-fun |state_2| () |state_type|)
+(declare-fun |state_3| () |state_type|)
+(declare-fun |expr_40_0| () Int)
+(declare-fun |expr_41_0| () Int)
+(declare-fun |expr_42_1| () Bool)
+(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
+(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
+
+(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| a_7_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| x_9_1))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| (+ expr_21_0 expr_26_1)))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
+","0xfc1bb12654dfc0b142e8333707b7c76c962a0d69fce4ca1d7290033f6cceb4e5":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_1| () Int)
+(declare-fun |x_9_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_26_1| () Int)
+(declare-fun |expr_27_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_31_1| () Int)
+(declare-fun |expr_33_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |state_1| () |state_type|)
+(declare-fun |state_2| () |state_type|)
+(declare-fun |state_3| () |state_type|)
+(declare-fun |expr_40_0| () Int)
+(declare-fun |expr_41_0| () Int)
+(declare-fun |expr_42_1| () Bool)
+(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
+(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
+
+(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))) (= expr_30_0 0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| a_7_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| x_9_1))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| expr_30_0))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
+"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
+ --> A:7:15:
+  |
+7 | \t\t\t\t\t\trequire(x >= 0);
+  | \t\t\t\t\t\t        ^^^^^^
+Note: Callstack:
+
+","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":196,"file":"A","start":190},"type":"Warning"},{"component":"general","errorCode":"4144","formattedMessage":"Warning: BMC: Underflow (resulting value less than 0) happens here.
+ --> A:8:7:
+  |
+8 | \t\t\t\t\t\t--x;
+  | \t\t\t\t\t\t^^^
+Note: Counterexample:
+  <result> = (- 1)
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+","message":"BMC: Underflow (resulting value less than 0) happens here.","secondarySourceLocations":[{"message":"Counterexample:
+  <result> = (- 1)
+  a = 0
+  x = 0
+"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"},{"component":"general","errorCode":"2661","formattedMessage":"Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+ --> A:9:7:
+  |
+9 | \t\t\t\t\t\tx + type(uint).max;
+  | \t\t\t\t\t\t^^^^^^^^^^^^^^^^^^
+Note: Counterexample:
+  <result> = 2**256
+  a = 0
+  x = 1
+
+Note: Callstack:
+Note:
+
+","message":"BMC: Overflow (resulting value larger than 2**256 - 1) happens here.","secondarySourceLocations":[{"message":"Counterexample:
+  <result> = 2**256
+  a = 0
+  x = 1
+"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"},{"component":"general","errorCode":"3046","formattedMessage":"Warning: BMC: Division by zero happens here.
+  --> A:10:7:
+   |
+10 | \t\t\t\t\t\t2 / x;
+   | \t\t\t\t\t\t^^^^^
+Note: Counterexample:
+  <result> = 0
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+","message":"BMC: Division by zero happens here.","secondarySourceLocations":[{"message":"Counterexample:
+  <result> = 0
+  a = 0
+  x = 0
+"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"},{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
+  --> A:11:7:
+   |
+11 | \t\t\t\t\t\ta.transfer(x);
+   | \t\t\t\t\t\t^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
+  a = 0
+  x = 0
+"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":268,"file":"A","start":255},"type":"Warning"},{"component":"general","errorCode":"4661","formattedMessage":"Warning: BMC: Assertion violation happens here.
+  --> A:12:7:
+   |
+12 | \t\t\t\t\t\tassert(x > 0);
+   | \t\t\t\t\t\t^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
+  a = 0
+  x = 0
+"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_all_chc/input.json

@@ -0,0 +1,29 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "chc",
+			"targets": "all"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_all_chc/output.json

@@ -0,0 +1,121 @@
+{"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)
+ --> A:8:7:
+  |
+8 | \t\t\t\t\t\t--x;
+  | \t\t\t\t\t\t^^^
+
+","message":"CHC: Underflow (resulting value less than 0) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 0)","severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)
+ --> A:9:7:
+  |
+9 | \t\t\t\t\t\tx + type(uint).max;
+  | \t\t\t\t\t\t^^^^^^^^^^^^^^^^^^
+
+","message":"CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+Counterexample:
+arr = []
+a = 0
+x = 1
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 2)","severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> A:10:7:
+   |
+10 | \t\t\t\t\t\t2 / x;
+   | \t\t\t\t\t\t^^^^^
+
+","message":"CHC: Division by zero happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)","severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> A:12:7:
+   |
+12 | \t\t\t\t\t\tassert(x > 0);
+   | \t\t\t\t\t\t^^^^^^^^^^^^^
+
+","message":"CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> A:13:7:
+   |
+13 | \t\t\t\t\t\tarr.pop();
+   | \t\t\t\t\t\t^^^^^^^^^
+
+","message":"CHC: Empty array \"pop\" happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json

@@ -0,0 +1,29 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "bmc",
+			"targets": "assert"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_assert_bmc/output.json

@@ -0,0 +1,70 @@
+{"auxiliaryInputRequested":{"smtlib2queries":{"0xa11872d9caace0479351e125d6feeb0d28b2b5e28bca4eb8b19c0139c4f94594":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_1| () Int)
+(declare-fun |x_9_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_26_1| () Int)
+(declare-fun |expr_27_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_31_1| () Int)
+(declare-fun |expr_33_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |state_1| () |state_type|)
+(declare-fun |state_2| () |state_type|)
+(declare-fun |state_3| () |state_type|)
+(declare-fun |expr_40_0| () Int)
+(declare-fun |expr_41_0| () Int)
+(declare-fun |expr_42_1| () Bool)
+(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
+(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
+
+(assert (and (and (and true true) (and (= expr_42_1 (> expr_40_0 expr_41_0)) (and (implies (and true true) true) (and (= expr_41_0 0) (and (implies (and true true) (and (>= expr_40_0 0) (<= expr_40_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_40_0 x_9_1) (and (= state_3 (ite (= this_0 expr_33_0) state_0 state_2)) (and (= state_2 (|state_type| (store (|balances| state_1) expr_33_0 (+ (select (|balances| state_1) expr_33_0) expr_36_0)))) (and (= state_1 (|state_type| (store (|balances| state_0) this_0 (+ (select (|balances| state_0) this_0) (- 0 expr_36_0))))) (and (and (>= (select (|balances| state_0) this_0) 0) (<= (select (|balances| state_0) this_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) true) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true))))))))))))))))))))))))))))))))))))))))))) (not expr_42_1)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| a_7_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| x_9_1))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
+"}},"errors":[{"component":"general","errorCode":"4661","formattedMessage":"Warning: BMC: Assertion violation happens here.
+  --> A:12:7:
+   |
+12 | \t\t\t\t\t\tassert(x > 0);
+   | \t\t\t\t\t\t^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
+  a = 0
+  x = 0
+"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json

@@ -0,0 +1,29 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "chc",
+			"targets": "assert"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json

@@ -0,0 +1,25 @@
+{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)
+  --> A:12:7:
+   |
+12 | \t\t\t\t\t\tassert(x > 0);
+   | \t\t\t\t\t\t^^^^^^^^^^^^^
+
+","message":"CHC: Assertion violation happens here.
+Counterexample:
+arr = []
+a = 0
+x = 0
+
+Transaction trace:
+test.constructor()
+State: arr = []
+test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json

@@ -0,0 +1,29 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "bmc",
+			"targets": "balance"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_balance_bmc/output.json

@@ -0,0 +1,70 @@
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x0a6e9ee4fe334d65b2abe8c35c92729ad3012940f546f260167f1d47d3746bd9":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_1| () Int)
+(declare-fun |x_9_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_26_1| () Int)
+(declare-fun |expr_27_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_31_1| () Int)
+(declare-fun |expr_33_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |state_1| () |state_type|)
+(declare-fun |state_2| () |state_type|)
+(declare-fun |state_3| () |state_type|)
+(declare-fun |expr_40_0| () Int)
+(declare-fun |expr_41_0| () Int)
+(declare-fun |expr_42_1| () Bool)
+(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
+(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
+(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
+
+(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) true) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| a_7_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| x_9_1))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
+"}},"errors":[{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
+  --> A:11:7:
+   |
+11 | \t\t\t\t\t\ta.transfer(x);
+   | \t\t\t\t\t\t^^^^^^^^^^^^^
+Note: Counterexample:
+  a = 0
+  x = 0
+
+Note: Callstack:
+Note:
+
+","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
+  a = 0
+  x = 0
+"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":268,"file":"A","start":255},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json

@@ -0,0 +1,29 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "chc",
+			"targets": "balance"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json

@@ -0,0 +1 @@
+{"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json

@@ -0,0 +1,29 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "bmc",
+			"targets": "constantCondition"
+		}
+	}
+}

test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/output.json

@@ -0,0 +1,58 @@
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x35cba50832f92f2e4e2c62c810158291d12ee4cb303a48798b61fa8c7945d055":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) (not expr_15_1)))
+(check-sat)
+","0xad522252173a6aa6ab3a770ff3f11427f810c4f5db7e6e5f639c8a21962b28f5":"(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
+(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
+(declare-fun |a_7_0| () Int)
+(declare-fun |x_9_0| () Int)
+(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_0| () Int)
+(declare-fun |expr_15_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) expr_15_1))
+(check-sat)
+"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
+ --> A:7:15:
+  |
+7 | \t\t\t\t\t\trequire(x >= 0);
+  | \t\t\t\t\t\t        ^^^^^^
+Note: Callstack:
+
+","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":196,"file":"A","start":190},"type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json

@@ -0,0 +1,29 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "chc",
+			"targets": "constantCondition"
+		}
+	}
+}