diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index ec10b44de..de80dd996 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -162,6 +162,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
 		smtutil::Expression constraints = m_context.assertions();
 		checkVerificationTargets(constraints);
 		m_verificationTargets.clear();
+		m_pathConditions.clear();
 	}
 
 	SMTEncoder::endVisit(_function);
@@ -184,7 +185,26 @@ bool BMC::visit(IfStatement const& _node)
 		);
 	m_context.popSolver();
 
-	SMTEncoder::visit(_node);
+	_node.condition().accept(*this);
+	auto conditionExpr = expr(_node.condition());
+	// visit true branch
+	auto [indicesEndTrue, trueEndPathCondition] = visitBranch(&_node.trueStatement(), conditionExpr);
+	auto touchedVars = touchedVariables(_node.trueStatement());
+
+	// visit false branch
+	decltype(indicesEndTrue) indicesEndFalse;
+	auto falseEndPathCondition = currentPathConditions() && !conditionExpr;
+	if (_node.falseStatement())
+	{
+		std::tie(indicesEndFalse, falseEndPathCondition) = visitBranch(_node.falseStatement(), !conditionExpr);
+		touchedVars += touchedVariables(*_node.falseStatement());
+	}
+	else
+		indicesEndFalse = copyVariableIndices();
+
+	// merge the information from branches
+	setPathCondition(trueEndPathCondition || falseEndPathCondition);
+	mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
 
 	return false;
 }
@@ -224,7 +244,7 @@ bool BMC::visit(WhileStatement const& _node)
 	decltype(indicesBeforeLoop) indicesAfterLoop;
 	if (_node.isDoWhile())
 	{
-		indicesAfterLoop = visitBranch(&_node.body());
+		indicesAfterLoop = visitBranch(&_node.body()).first;
 		// TODO the assertions generated in the body should still be active in the condition
 		_node.condition().accept(*this);
 		if (isRootFunction())
@@ -244,7 +264,7 @@ bool BMC::visit(WhileStatement const& _node)
 				&_node.condition()
 			);
 
-		indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition()));
+		indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition())).first;
 	}
 
 	// We reset the execution to before the loop
@@ -406,6 +426,12 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	}
 }
 
+void BMC::endVisit(Return const& _return)
+{
+	SMTEncoder::endVisit(_return);
+	setPathCondition(smtutil::Expression(false));
+}
+
 /// Visitor helpers.
 
 void BMC::visitAssert(FunctionCall const& _funCall)
@@ -467,7 +493,9 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
 		// is that there we don't have `_funCall`.
 		pushCallStack({funDef, &_funCall});
+		pushPathCondition(currentPathConditions());
 		funDef->accept(*this);
+		popPathCondition();
 	}
 
 	createReturnedExpressions(_funCall);
@@ -968,3 +996,14 @@ smtutil::CheckResult BMC::checkSatisfiable()
 	return checkSatisfiableAndGenerateModel({}).first;
 }
 
+void BMC::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value)
+{
+	auto oldVar = _symVar.currentValue();
+	auto newVar = _symVar.increaseIndex();
+	m_context.addAssertion(smtutil::Expression::ite(
+		currentPathConditions(),
+		newVar == _value,
+		newVar == oldVar
+	));
+}
+
diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
index d55ce7666..3bdd0caa9 100644
--- a/libsolidity/formal/BMC.h
+++ b/libsolidity/formal/BMC.h
@@ -90,6 +90,7 @@ private:
 	bool visit(ForStatement const& _node) override;
 	void endVisit(UnaryOperation const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
+	void endVisit(Return const& _node) override;
 	//@}
 
 	/// Visitor helpers.
@@ -97,6 +98,7 @@ private:
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
 	void visitAddMulMod(FunctionCall const& _funCall) override;
+	void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value) override;
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 44d4d4be6..d2e463b23 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -155,8 +155,10 @@ void SMTEncoder::visitFunctionOrModifier()
 
 	if (m_modifierDepthStack.back() == static_cast<int>(function.modifiers().size()))
 	{
+		pushPathCondition(currentPathConditions());
 		if (function.isImplemented())
 			function.body().accept(*this);
+		popPathCondition();
 	}
 	else
 	{
@@ -193,6 +195,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 	initializeFunctionCallParameters(*_definition, args);
 
 	pushCallStack({_definition, _invocation});
+	pushPathCondition(currentPathConditions());
 	if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
 	{
 		if (modifier->isImplemented())
@@ -205,6 +208,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 			function->accept(*this);
 		// Functions are popped from the callstack in endVisit(FunctionDefinition)
 	}
+	popPathCondition();
 }
 
 void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
@@ -288,26 +292,6 @@ bool SMTEncoder::visit(TryCatchClause const& _clause)
 	return false;
 }
 
-bool SMTEncoder::visit(IfStatement const& _node)
-{
-	_node.condition().accept(*this);
-
-	auto indicesEndTrue = visitBranch(&_node.trueStatement(), expr(_node.condition()));
-	auto touchedVars = touchedVariables(_node.trueStatement());
-	decltype(indicesEndTrue) indicesEndFalse;
-	if (_node.falseStatement())
-	{
-		indicesEndFalse = visitBranch(_node.falseStatement(), !expr(_node.condition()));
-		touchedVars += touchedVariables(*_node.falseStatement());
-	}
-	else
-		indicesEndFalse = copyVariableIndices();
-
-	mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
-
-	return false;
-}
-
 void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 {
 	if (_varDecl.declarations().size() != 1)
@@ -598,10 +582,10 @@ bool SMTEncoder::visit(Conditional const& _op)
 {
 	_op.condition().accept(*this);
 
-	auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition()));
+	auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first;
 	auto touchedVars = touchedVariables(_op.trueExpression());
 
-	auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition()));
+	auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first;
 	touchedVars += touchedVariables(_op.falseExpression());
 
 	mergeVariables(touchedVars, expr(_op.condition()), indicesEndTrue, indicesEndFalse);
@@ -1754,13 +1738,13 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
 		_op.leftExpression().accept(*this);
 		if (_op.getOperator() == Token::And)
 		{
-			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression()));
+			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
 			mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
 		}
 		else
 		{
-			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression()));
+			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
 			mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
 		}
@@ -1974,22 +1958,29 @@ void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression
 	m_context.addAssertion(_symVar.increaseIndex() == _value);
 }
 
-SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition)
+pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
+	ASTNode const* _statement,
+	smtutil::Expression _condition
+)
 {
 	return visitBranch(_statement, &_condition);
 }
 
-SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition)
+pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
+	ASTNode const* _statement,
+	smtutil::Expression const* _condition
+)
 {
 	auto indicesBeforeBranch = copyVariableIndices();
 	if (_condition)
 		pushPathCondition(*_condition);
 	_statement->accept(*this);
+	auto pathConditionOnExit = currentPathConditions();
 	if (_condition)
 		popPathCondition();
 	auto indicesAfterBranch = copyVariableIndices();
 	resetVariableIndices(indicesBeforeBranch);
-	return indicesAfterBranch;
+	return {indicesAfterBranch, pathConditionOnExit};
 }
 
 void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs)
@@ -2245,6 +2236,14 @@ void SMTEncoder::pushPathCondition(smtutil::Expression const& _e)
 	m_pathConditions.push_back(currentPathConditions() && _e);
 }
 
+void SMTEncoder::setPathCondition(smtutil::Expression const& _e)
+{
+	if (m_pathConditions.empty())
+		m_pathConditions.push_back(_e);
+	else
+		m_pathConditions.back() = _e;
+}
+
 smtutil::Expression SMTEncoder::currentPathConditions()
 {
 	if (m_pathConditions.empty())
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 8dffc2682..4c26cb4c8 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -89,7 +89,7 @@ protected:
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
 	bool visit(PlaceholderStatement const& _node) override;
-	bool visit(IfStatement const& _node) override;
+	bool visit(IfStatement const&) override { return false; }
 	bool visit(WhileStatement const&) override { return false; }
 	bool visit(ForStatement const&) override { return false; }
 	void endVisit(VariableDeclarationStatement const& _node) override;
@@ -197,7 +197,7 @@ protected:
 
 	/// Handles the actual assertion of the new value to the encoding context.
 	/// Other assignment methods should use this one in the end.
-	void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
+	virtual void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
 
 	void assignment(VariableDeclaration const& _variable, Expression const& _value);
 	/// Handles assignments to variables of different types.
@@ -219,9 +219,10 @@ protected:
 
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
-	/// @returns the variable indices after visiting the branch.
-	VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
-	VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
+	/// @returns the variable indices after visiting the branch and the expression representing
+	/// the path condition at the end of the branch.
+	std::pair<VariableIndices, smtutil::Expression> visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
+	std::pair<VariableIndices, smtutil::Expression> visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
 
 	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
 
@@ -263,6 +264,8 @@ protected:
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smtutil::Expression _value);
 
+	/// Overwrites the current path condition
+	void setPathCondition(smtutil::Expression const& _e);
 	/// Adds a new path condition
 	void pushPathCondition(smtutil::Expression const& _e);
 	/// Remove the last path condition
diff --git a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
index 63a21eb4e..8840c2477 100644
--- a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
+++ b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
@@ -1,4 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x8b2c3058077c75f8fff85d2d387198b91b4e591448624f4bef0ab6c7b87d5ec1":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x238aade411d63d50406236089e28f3770d51f95888222fdb838f930911e0f763":"(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -15,7 +15,7 @@
 (declare-fun |expr_9_0| () Int)
 (declare-fun |expr_10_1| () Bool)
 
-(assert (and (and true (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (= expr_9_0 0) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))) (not expr_10_1)))
+(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (= expr_9_0 0) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))) (not expr_10_1)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (check-sat)
diff --git a/test/cmdlineTests/standard_model_checker_timeout_all/output.json b/test/cmdlineTests/standard_model_checker_timeout_all/output.json
index e055cb70b..1f9d232fe 100644
--- a/test/cmdlineTests/standard_model_checker_timeout_all/output.json
+++ b/test/cmdlineTests/standard_model_checker_timeout_all/output.json
@@ -1,4 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x0ab92bf00d2546a23d94ff3a406d009299b43650e321d35e02531726df040b9d":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x0d6f843ef6990bfad1918be96d1aad42b5d7ca87a171d0ac34009e0d4b6e8e03":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -26,9 +26,9 @@
 (declare-fun |expr_21_0| () Int)
 (declare-fun |expr_22_1| () Bool)
 
-(assert (and (and true (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
+(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
 (check-sat)
-","0x34467f46a484d40c850f05c3b05b0817a859573bc546982aeab4a17f9259fb5b":"(set-option :produce-models true)
+","0x3091365cefd5a713eea87735305ab53c75303343ebf74b77d3578ae0b73c64a2":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -49,9 +49,99 @@
 (declare-fun |expr_13_0| () Int)
 (declare-fun |expr_14_1| () Bool)
 
-(assert (and (and true (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
+(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
 (check-sat)
-","0x3dd3d755e279cd0bf414fd3fd9830517ee2397e3931ec76a9fd970b5eec46384":"(set-option :produce-models true)
+","0x6b268fc2d87ebda3f3b3b93c8d0b2b5374fd3bd33387113b9ee138a85c142dae":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_15_0| () Int)
+(declare-fun |r_div_mod_15_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_16_0| () Int)
+(declare-fun |r_div_mod_16_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
+(check-sat)
+","0xa81ce8317a79fc74d85d9edfe56caf9b0274a7da4556bfb418652051e0bfa679":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
+(check-sat)
+","0xaec7aba847ba235b585e4c7e6ec8d8eee964e76bd40a02e00af3354acede95d8":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_15_0| () Int)
+(declare-fun |r_div_mod_15_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
+(check-sat)
+","0xe6aad7b5a7ba681908e47e11921c93815f9a4cdd90ef82dd79a60fcac94492c9":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -102,7 +192,7 @@
 (declare-fun |expr_45_0| () Int)
 (declare-fun |expr_46_1| () Bool)
 
-(assert (and (and true (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_18_0)) (and (and (<= 0 r_div_mod_18_0) (or (= expr_43_0 0) (< r_div_mod_18_0 expr_43_0))) (and (= (+ (* d_div_mod_18_0 expr_43_0) r_div_mod_18_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (= r_34_1 expr_39_1) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_17_0)) (and (and (<= 0 r_div_mod_17_0) (or (= expr_38_0 0) (< r_div_mod_17_0 expr_38_0))) (and (= (+ (* d_div_mod_17_0 expr_38_0) r_div_mod_17_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies true expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
+(assert (and (and (and true true) (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_18_0)) (and (and (<= 0 r_div_mod_18_0) (or (= expr_43_0 0) (< r_div_mod_18_0 expr_43_0))) (and (= (+ (* d_div_mod_18_0 expr_43_0) r_div_mod_18_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_17_0)) (and (and (<= 0 r_div_mod_17_0) (or (= expr_38_0 0) (< r_div_mod_17_0 expr_38_0))) (and (= (+ (* d_div_mod_17_0 expr_38_0) r_div_mod_17_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (declare-const |EVALEXPR_1| Int)
@@ -113,7 +203,7 @@
 (assert (= |EVALEXPR_3| r_34_1))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
-","0x4b82600501b4619c19bf57eb8d3cdb69f1c0d2a807d5908f1503d07e65ce2fd6":"(set-option :produce-models true)
+","0xf877f10b1dc480ae2403c9376947f543da579bf3aff7dfaa2f946e300b81d305":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -148,97 +238,7 @@
 (declare-fun |expr_29_0| () Int)
 (declare-fun |expr_30_1| () Bool)
 
-(assert (and (and true (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
-(check-sat)
-","0x5d4ad2f9c711b9e187dba2577e849272617d56d0ba3d46427baa3c11804a9143":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_15_0| () Int)
-(declare-fun |r_div_mod_15_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-
-(assert (and (and true (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
-(check-sat)
-","0xd63dd6c8c7f21f7200de074c7131ab703fcb783425bc609ee7541efc2fc320bf":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_15_0| () Int)
-(declare-fun |r_div_mod_15_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_16_0| () Int)
-(declare-fun |r_div_mod_16_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-
-(assert (and (and true (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
-(check-sat)
-","0xee7d96e23195f6aeb74a805122639dcd6a8932788ceeae3cba711aba9050a0b7":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-
-(assert (and (and true (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
+(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
 (check-sat)
 "}},"errors":[{"component":"general","errorCode":"6328","formattedMessage":"A:6:85: Warning: CHC: Assertion violation might happen here.
 require(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}}
diff --git a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
index b1db514d4..e59ff2f82 100644
--- a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
+++ b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
@@ -1,78 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x0f5149c7799751d1575c0946ca73f9a1a9dbc6c432db3c5e13625bd301d7fd37":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-
-(assert (and (and true (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
-(check-sat)
-","0x11444b207b7d8827f8b7503cad8aed1426a8727290a070d1eed04a55e85e2f14":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-
-(assert (and (and true (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
-(check-sat)
-","0x317d72a016f7a5ff016cda82e96601cfac3a0498f393852410c7ce335d4896c8":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x0e2ec6d70e3de7ac14f07c9bbb08f9436e3b832ae8456d340e4d4a8b8712c7f5":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -123,280 +49,7 @@
 (declare-fun |expr_45_0| () Int)
 (declare-fun |expr_46_1| () Bool)
 
-(assert (and (and true (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (= r_34_1 expr_39_1) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies true expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))))))))) (= expr_43_0 0)))
-(declare-const |EVALEXPR_0| Int)
-(assert (= |EVALEXPR_0| x_4_0))
-(declare-const |EVALEXPR_1| Int)
-(assert (= |EVALEXPR_1| y_6_0))
-(declare-const |EVALEXPR_2| Int)
-(assert (= |EVALEXPR_2| k_8_0))
-(declare-const |EVALEXPR_3| Int)
-(assert (= |EVALEXPR_3| r_34_1))
-(declare-const |EVALEXPR_4| Int)
-(assert (= |EVALEXPR_4| expr_43_0))
-(check-sat)
-(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0x34467f46a484d40c850f05c3b05b0817a859573bc546982aeab4a17f9259fb5b":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-
-(assert (and (and true (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
-(check-sat)
-","0x46b3448dbd021b48635faf7ba42511a38684819cde3808197301d93fa7b482ea":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-
-(assert (and (and true (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
-(check-sat)
-","0x6929232f73f56b073cf47977f8ce4ce5c728e02e72812041b60b544333443c3c":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
-(declare-fun |expr_36_0| () Int)
-(declare-fun |expr_37_0| () Int)
-(declare-fun |expr_38_0| () Int)
-(declare-fun |d_div_mod_2_0| () Int)
-(declare-fun |r_div_mod_2_0| () Int)
-(declare-fun |expr_39_1| () Int)
-(declare-fun |r_34_1| () Int)
-(declare-fun |expr_42_0| () Int)
-(declare-fun |expr_43_0| () Int)
-(declare-fun |d_div_mod_3_0| () Int)
-(declare-fun |r_div_mod_3_0| () Int)
-(declare-fun |expr_44_1| () Int)
-(declare-fun |expr_45_0| () Int)
-(declare-fun |expr_46_1| () Bool)
-
-(assert (and (and true (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_3_0)) (and (and (<= 0 r_div_mod_3_0) (or (= expr_43_0 0) (< r_div_mod_3_0 expr_43_0))) (and (= (+ (* d_div_mod_3_0 expr_43_0) r_div_mod_3_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (= r_34_1 expr_39_1) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies true expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
-(declare-const |EVALEXPR_0| Int)
-(assert (= |EVALEXPR_0| x_4_0))
-(declare-const |EVALEXPR_1| Int)
-(assert (= |EVALEXPR_1| y_6_0))
-(declare-const |EVALEXPR_2| Int)
-(assert (= |EVALEXPR_2| k_8_0))
-(declare-const |EVALEXPR_3| Int)
-(assert (= |EVALEXPR_3| r_34_1))
-(check-sat)
-(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
-","0x7d43d079635c11d55bba40ba4b7f9c9beeef336e19e5612f020ab7547affbf54":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-
-(assert (and (and true (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
-(check-sat)
-","0x94d4c42b833aeec4b7c67fb46410594966e252d7ca8bf44e5687142a078842b2":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
-(declare-fun |expr_36_0| () Int)
-(declare-fun |expr_37_0| () Int)
-(declare-fun |expr_38_0| () Int)
-(declare-fun |d_div_mod_2_0| () Int)
-(declare-fun |r_div_mod_2_0| () Int)
-(declare-fun |expr_39_1| () Int)
-(declare-fun |r_34_1| () Int)
-(declare-fun |expr_42_0| () Int)
-(declare-fun |expr_43_0| () Int)
-(declare-fun |d_div_mod_3_0| () Int)
-(declare-fun |r_div_mod_3_0| () Int)
-(declare-fun |expr_44_1| () Int)
-(declare-fun |expr_45_0| () Int)
-(declare-fun |expr_46_1| () Bool)
-
-(assert (and (and true (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies true expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))) (= expr_38_0 0)))
-(declare-const |EVALEXPR_0| Int)
-(assert (= |EVALEXPR_0| x_4_0))
-(declare-const |EVALEXPR_1| Int)
-(assert (= |EVALEXPR_1| y_6_0))
-(declare-const |EVALEXPR_2| Int)
-(assert (= |EVALEXPR_2| k_8_0))
-(declare-const |EVALEXPR_3| Int)
-(assert (= |EVALEXPR_3| r_34_0))
-(declare-const |EVALEXPR_4| Int)
-(assert (= |EVALEXPR_4| expr_38_0))
-(check-sat)
-(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0x9ccee337d79bf0618f658506fca4179eacaee0de28aebc060fce24a9a2cb21fc":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(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.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-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
-(declare-fun |expr_36_0| () Int)
-(declare-fun |expr_37_0| () Int)
-(declare-fun |expr_38_0| () Int)
-(declare-fun |d_div_mod_2_0| () Int)
-(declare-fun |r_div_mod_2_0| () Int)
-(declare-fun |expr_39_1| () Int)
-(declare-fun |r_34_1| () Int)
-(declare-fun |expr_42_0| () Int)
-(declare-fun |expr_43_0| () Int)
-(declare-fun |d_div_mod_3_0| () Int)
-(declare-fun |r_div_mod_3_0| () Int)
-(declare-fun |expr_44_1| () Int)
-(declare-fun |expr_45_0| () Int)
-(declare-fun |expr_46_1| () Bool)
-
-(assert (and (and true (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))) (= expr_27_0 0)))
+(assert (and (and (and true true) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))) (= expr_27_0 0)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (declare-const |EVALEXPR_1| Int)
@@ -409,7 +62,30 @@
 (assert (= |EVALEXPR_4| expr_27_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0xc087609e1dc5e5b58588a60985e4e04dbb5b602e92873c2123a018895f5f9e1a":"(set-option :produce-models true)
+","0x3091365cefd5a713eea87735305ab53c75303343ebf74b77d3578ae0b73c64a2":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
+(check-sat)
+","0x46c0f34a4da6b31138e9238be92256a3c472a5a24c88371ef680f78e0c520cb6":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -460,7 +136,205 @@
 (declare-fun |expr_45_0| () Int)
 (declare-fun |expr_46_1| () Bool)
 
-(assert (and (and true (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))) (= expr_19_0 0)))
+(assert (and (and (and true true) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))) (= expr_38_0 0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| x_4_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| y_6_0))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| k_8_0))
+(declare-const |EVALEXPR_3| Int)
+(assert (= |EVALEXPR_3| r_34_0))
+(declare-const |EVALEXPR_4| Int)
+(assert (= |EVALEXPR_4| expr_38_0))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
+","0x6378f27de46d517b5bafe774eab66c12cb656dbd031cb5e710f07b1bfd6c5f79":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
+(check-sat)
+","0x7db419e89d4bb9fbaa4bda7fd522223a515177ff577a6d381e7f2b7f4612582b":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
+(check-sat)
+","0x7de8eaf2518b47eec1afadbebacdfa7d93a1878e0f1b6eef91b8a80f1246937e":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
+(check-sat)
+","0x8c4f3faef8ad4a2fe9935f16ec93e2df20f5a3831be51c13afe060774658141c":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
+(check-sat)
+","0xa4666c5d197afd69bd82af703fb694c1d3cdd8926ab480fc42e69231134d9265":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |expr_37_0| () Int)
+(declare-fun |expr_38_0| () Int)
+(declare-fun |d_div_mod_2_0| () Int)
+(declare-fun |r_div_mod_2_0| () Int)
+(declare-fun |expr_39_1| () Int)
+(declare-fun |r_34_1| () Int)
+(declare-fun |expr_42_0| () Int)
+(declare-fun |expr_43_0| () Int)
+(declare-fun |d_div_mod_3_0| () Int)
+(declare-fun |r_div_mod_3_0| () Int)
+(declare-fun |expr_44_1| () Int)
+(declare-fun |expr_45_0| () Int)
+(declare-fun |expr_46_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))) (= expr_19_0 0)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (declare-const |EVALEXPR_1| Int)
@@ -473,7 +347,7 @@
 (assert (= |EVALEXPR_4| expr_19_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0xee7d96e23195f6aeb74a805122639dcd6a8932788ceeae3cba711aba9050a0b7":"(set-option :produce-models true)
+","0xa81ce8317a79fc74d85d9edfe56caf9b0274a7da4556bfb418652051e0bfa679":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -494,8 +368,134 @@
 (declare-fun |expr_13_0| () Int)
 (declare-fun |expr_14_1| () Bool)
 
-(assert (and (and true (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
+(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
 (check-sat)
+","0xa96a68b7853fcc0a10dd525c3ff838e3bfac425b104c44b240623f7a35aee6f1":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |expr_37_0| () Int)
+(declare-fun |expr_38_0| () Int)
+(declare-fun |d_div_mod_2_0| () Int)
+(declare-fun |r_div_mod_2_0| () Int)
+(declare-fun |expr_39_1| () Int)
+(declare-fun |r_34_1| () Int)
+(declare-fun |expr_42_0| () Int)
+(declare-fun |expr_43_0| () Int)
+(declare-fun |d_div_mod_3_0| () Int)
+(declare-fun |r_div_mod_3_0| () Int)
+(declare-fun |expr_44_1| () Int)
+(declare-fun |expr_45_0| () Int)
+(declare-fun |expr_46_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_3_0)) (and (and (<= 0 r_div_mod_3_0) (or (= expr_43_0 0) (< r_div_mod_3_0 expr_43_0))) (and (= (+ (* d_div_mod_3_0 expr_43_0) r_div_mod_3_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| x_4_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| y_6_0))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| k_8_0))
+(declare-const |EVALEXPR_3| Int)
+(assert (= |EVALEXPR_3| r_34_1))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
+","0xcc1de975d2f5e9b3e4ff9b4f46c8248513ac3b755b60f8a630a46d12b4b11f9a":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(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.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-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |expr_37_0| () Int)
+(declare-fun |expr_38_0| () Int)
+(declare-fun |d_div_mod_2_0| () Int)
+(declare-fun |r_div_mod_2_0| () Int)
+(declare-fun |expr_39_1| () Int)
+(declare-fun |r_34_1| () Int)
+(declare-fun |expr_42_0| () Int)
+(declare-fun |expr_43_0| () Int)
+(declare-fun |d_div_mod_3_0| () Int)
+(declare-fun |r_div_mod_3_0| () Int)
+(declare-fun |expr_44_1| () Int)
+(declare-fun |expr_45_0| () Int)
+(declare-fun |expr_46_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))))))))) (= expr_43_0 0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| x_4_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| y_6_0))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| k_8_0))
+(declare-const |EVALEXPR_3| Int)
+(assert (= |EVALEXPR_3| r_34_1))
+(declare-const |EVALEXPR_4| Int)
+(assert (= |EVALEXPR_4| expr_43_0))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
 "}},"errors":[{"component":"general","errorCode":"7812","formattedMessage":"A:6:85: Warning: BMC: Assertion violation might happen here.
 require(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}}
                                                                                     ^----------------^
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers.sol
new file mode 100644
index 000000000..fb87df2b5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers.sol
@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+
+	modifier check() {
+		require(x == 0);
+		_;
+		assert(x == 1); // should fail;
+		assert(x == 0); // should hold;
+	}
+
+	modifier inc() {
+		if (x == 0) {
+			return;
+		}
+		x = x + 1;
+		_;
+	}
+
+	function test() check inc public {
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (103-117): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers_2.sol
new file mode 100644
index 000000000..47e3a27ef
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers_2.sol
@@ -0,0 +1,45 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+    uint x;
+
+    function reset_if_overflow() internal postinc {
+        if (x < 10)
+            return;
+        x = 0;
+    }
+
+    modifier postinc() {
+        if (x == 0) {
+            return;
+        }
+        _;
+        x = x + 1;
+    }
+
+    function test() public {
+        if (x == 0) {
+            reset_if_overflow();
+            assert(x == 1); // should fail;
+            assert(x == 0); // should hold;
+            return;
+        }
+        if (x < 10) {
+            uint oldx = x;
+            reset_if_overflow();
+            assert(oldx + 1 == x); // should hold;
+            assert(oldx == x);     // should fail;
+            return;
+        }
+        reset_if_overflow();
+        assert(x == 1); // should hold;
+        assert(x == 0); // should fail;
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (384-398): BMC: Assertion violation happens here.
+// Warning 4661: (635-652): BMC: Assertion violation happens here.
+// Warning 4661: (781-795): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
new file mode 100644
index 000000000..6d960112a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
@@ -0,0 +1,43 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int x;
+	constructor (int a) { x = a;}
+}
+
+contract B is A {
+	int y;
+	constructor(int a) A(-a) {
+		if (a > 0) {
+			y = 2;
+			return;
+		}
+		else {
+			y = 3;
+		}
+		y = 4; // overwrites the else branch
+	}
+}
+
+contract C is B {
+	constructor(int a) B(a) {
+		assert(y != 3); // should hold
+		assert(y == 4); // should fail
+		if (a > 0) {
+			assert(x < 0 && y == 2); // should hold
+			assert(x < 0 && y == 4); // should fail
+		}
+		else {
+			assert(x >= 0 && y == 4); // should hold
+			assert(x >= 0 && y == 2); // should fail
+			assert(x > 0); // should fail
+		}
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (330-344): BMC: Assertion violation happens here.
+// Warning 4661: (422-445): BMC: Assertion violation happens here.
+// Warning 4661: (522-546): BMC: Assertion violation happens here.
+// Warning 4661: (566-579): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_chain_alternate.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_chain_alternate.sol
new file mode 100644
index 000000000..511cfbb60
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_chain_alternate.sol
@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x = 1;
+}
+
+contract B is A {
+	constructor(int a) {
+		if (a > 0) {
+			x = 2;
+			return;
+		}
+		x = 3;
+	}
+}
+
+abstract contract C is B {
+}
+
+contract D is C {
+	constructor(int a) B(a) {
+		assert(a > 0 || x == 3); // should hold
+		assert(a <= 0 || x == 2); // should hold
+		assert(x == 1); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (319-333): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_diamond.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_diamond.sol
new file mode 100644
index 000000000..c962d1003
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_diamond.sol
@@ -0,0 +1,72 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int x;
+}
+
+contract B is A {
+	int y;
+	constructor (int a) {
+		if (a >= 0) {
+			y = 1;
+			return;
+		}
+		x = 1;
+		y = 2;
+	}
+}
+
+contract C is A {
+	int z;
+	constructor (int a) {
+		if (a >= 0) {
+			z = 1;
+			return;
+		}
+		x = -1;
+		z = 2;
+	}
+}
+
+contract D1 is B, C {
+	constructor() B(1) C(1) {
+		assert(x == 0); // should hold
+		assert(x == 1); // should fail
+		assert(x == -1); // should fail
+	}
+}
+
+contract D2 is B, C {
+	constructor() B(1) C(-1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should fail
+		assert(x == -1); // should hold (constructor of C is executed AFTER constructor of B)
+	}
+}
+
+contract D3 is B, C {
+	constructor() B(-1) C(1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should hold
+		assert(x == -1); // should fail
+	}
+}
+
+contract D4 is B, C {
+	constructor() B(-1) C(-1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should fail
+		assert(x == -1); // should hold (constructor of C is executed AFTER constructor of B)
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (370-384): BMC: Assertion violation happens here.
+// Warning 4661: (403-418): BMC: Assertion violation happens here.
+// Warning 4661: (493-507): BMC: Assertion violation happens here.
+// Warning 4661: (526-540): BMC: Assertion violation happens here.
+// Warning 4661: (703-717): BMC: Assertion violation happens here.
+// Warning 4661: (769-784): BMC: Assertion violation happens here.
+// Warning 4661: (860-874): BMC: Assertion violation happens here.
+// Warning 4661: (893-907): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructors.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructors.sol
new file mode 100644
index 000000000..9ed5ddcbf
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructors.sol
@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract B {
+	int x;
+	constructor(int b) {
+		if (b > 0) {
+			x = 1;
+			return;
+		}
+		else {
+			x = 2;
+			return;
+		}
+		x = 3; // dead code
+	}
+}
+
+contract C is B {
+	constructor(int a) B(a) {
+		assert(a > 0 || x == 2); // should hold
+		assert(a <= 0 || x == 1); // should hold
+		assert(x == 3); // should fail
+		assert(x == 2); // should fail
+		assert(x == 1); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 5740: (152-157): Unreachable code.
+// Warning 4661: (310-324): BMC: Assertion violation happens here.
+// Warning 4661: (343-357): BMC: Assertion violation happens here.
+// Warning 4661: (376-390): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/nested_if.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/nested_if.sol
new file mode 100644
index 000000000..c941c6421
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/nested_if.sol
@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test(uint256 a, uint256 b) public pure {
+		assert(nested_if(a,b) != 42); // should hold
+		assert(nested_if(a,b) == 1);  // should fail
+	}
+
+	function nested_if(uint256 a, uint256 b) internal pure returns (uint256) {
+		if (a < 5) {
+			if (b > 1) {
+				return 0;
+			}
+		}
+		if (a == 2 && b == 2) {
+			return 42; // unreachable
+		}
+		else {
+			return 1;
+		}
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (147-174): BMC: Assertion violation happens here.
+// Warning 6838: (332-348): BMC: Condition is always false.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/return_in_both_branches.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/return_in_both_branches.sol
new file mode 100644
index 000000000..0ad554c31
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/return_in_both_branches.sol
@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test() public pure {
+		assert(branches(0) == 0);
+		assert(branches(1) == 42);
+	}
+
+	function branches(uint256 a) internal pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		else {
+			return 42;
+		}
+		return 1; // dead code
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 5740: (265-273): Unreachable code.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if.sol
new file mode 100644
index 000000000..783a28543
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function test(uint256 a, uint256 b) public pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		return b / a; // This division is safe because of the early return in if-block.
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if2.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if2.sol
new file mode 100644
index 000000000..d614edb55
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if2.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test(uint256 a) public pure {
+		assert(simple_if(a) == 1); // should fail for a == 0
+	}
+
+	function simple_if(uint256 a) internal pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		return 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (89-114): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_array.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_array.sol
new file mode 100644
index 000000000..70cc1ed38
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_array.sol
@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint[] a;
+
+	constructor () {
+		a.push();
+		a.push();
+	}
+
+	function check() public {
+		require(a.length >= 2);
+		require(a[1] == 0);
+		conditional_store();
+		assert(a[1] == 1); // should fail;
+		assert(a[1] == 0); // should hold;
+	}
+
+	function conditional_store() internal {
+		if (a[1] == 0) {
+			return;
+		}
+		a[1] = 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (205-222): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_state_var.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_state_var.sol
new file mode 100644
index 000000000..5acc7fcbe
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_state_var.sol
@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+
+	function check() public {
+		require(x == 0);
+		conditional_increment();
+		assert(x == 1); // should fail;
+		assert(x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (x == 0) {
+			return;
+		}
+		x = 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (132-146): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct.sol
new file mode 100644
index 000000000..de3cfda1b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct.sol
@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	struct S {
+		uint x;
+	}
+	S s;
+
+	function check() public {
+		require(s.x == 0);
+		conditional_increment();
+		assert(s.x == 1); // should fail;
+		assert(s.x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (s.x == 0) {
+			return;
+		}
+		s.x = 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (156-172): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct_2.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct_2.sol
new file mode 100644
index 000000000..d709be0c7
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct_2.sol
@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	struct S {
+		uint x;
+	}
+	S s;
+
+	function check() public {
+		require(s.x == 0);
+		conditional_increment();
+		assert(s.x == 1); // should fail;
+		assert(s.x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (s.x == 0) {
+			return;
+		}
+		s = S(1);
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (156-172): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_tuple.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_tuple.sol
new file mode 100644
index 000000000..e1e6b323c
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_tuple.sol
@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+	uint y;
+
+	function check() public {
+		require(x == 0);
+		require(y == 0);
+		conditional_increment();
+		assert(x == 0); // should fail;
+		assert(x == 1); // should fail;
+		assert(x == 2); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (x == 0) {
+			(x,y) = (2,2);
+			return;
+		}
+		(x,y) = (1,1);
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (160-174): BMC: Assertion violation happens here.
+// Warning 4661: (194-208): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/triple_nested_if.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/triple_nested_if.sol
new file mode 100644
index 000000000..38a5c852b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/triple_nested_if.sol
@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+    uint a;
+    uint b;
+    uint c;
+
+	function test() public view {
+		if (a == 0) {
+			if (b == 0) {
+				if (c == 0) {
+					return;
+				}
+			}
+		}
+		assert(a != 0 || b != 0 || c != 0);
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
diff --git a/test/libsolidity/smtCheckerTests/operators/division_6.sol b/test/libsolidity/smtCheckerTests/operators/division_6.sol
index 4dfd728c1..5672a9784 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_6.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_6.sol
@@ -1,14 +1,14 @@
 pragma experimental SMTChecker;
 contract C {
-	function mul(uint256 a, uint256 b) internal pure returns (uint256) {
+	function mul(uint256 a, uint256 b) public pure returns (uint256) {
 		if (a == 0) {
 			return 0;
 		}
-		// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
-		require(a != 0);
 		uint256 c = a * b;
 		require(c / a == b);
 		return c;
 	}
 }
 // ----
+// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4281: (177-182): CHC: Division by zero happens here.