From ecb90b69bdf01fd77183966f6fcdbf59bd180292 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Sun, 17 Apr 2022 18:25:27 +0200
Subject: [PATCH] fix multi assignmnets

---
 libyul/optimiser/ReasoningBasedSimplifier.cpp |  9 +++++++++
 libyul/optimiser/SMTSolver.cpp                | 18 ++++++++++++++++++
 libyul/optimiser/SMTSolver.h                  |  1 +
 3 files changed, 28 insertions(+)

diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index 546f515a5..7da511096 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -158,6 +158,15 @@ void ReasoningBasedSimplifier::operator()(FunctionDefinition& _fun)
 {
 	ScopedSaveAndRestore counters(m_variableSequenceCounter, {});
 	ScopedSaveAndRestore pathCond(m_pathCondition, true);
+	for (auto const& param: _fun.parameters)
+		encodeVariableUpdateUnknown(param.name);
+	for (auto const& retVar: _fun.returnVariables)
+	{
+		encodeVariableUpdateUnknown(retVar.name);
+		// TODO remove the redundant encoding above
+		m_solver->addAssertion(currentVariableExpression(retVar.name) == 0);
+	}
+
 	ASTModifier::operator()(_fun);
 }
 
diff --git a/libyul/optimiser/SMTSolver.cpp b/libyul/optimiser/SMTSolver.cpp
index 9c8ffacb5..9fee9a301 100644
--- a/libyul/optimiser/SMTSolver.cpp
+++ b/libyul/optimiser/SMTSolver.cpp
@@ -160,12 +160,19 @@ void SMTSolver::encodeVariableDeclaration(VariableDeclaration const& _varDecl)
 		_varDecl.value
 	)
 		encodeVariableUpdate(_varDecl.variables.front().name, *_varDecl.value);
+	else
+		for (auto const& var: _varDecl.variables)
+			encodeVariableUpdateUnknown(var.name);
+
 }
 
 void SMTSolver::encodeVariableAssignment(Assignment const& _assignment)
 {
 	if (_assignment.variableNames.size() == 1)
 		encodeVariableUpdate(_assignment.variableNames.front().name, *_assignment.value);
+	else
+		for (auto const& var: _assignment.variableNames)
+			encodeVariableUpdateUnknown(var.name);
 }
 
 void SMTSolver::encodeVariableUpdate(YulString const& _name, Expression const& _value)
@@ -179,3 +186,14 @@ void SMTSolver::encodeVariableUpdate(YulString const& _name, Expression const& _
 	m_solver->newVariable(variableNameAtIndex(_name, m_variableSequenceCounter[_name]), defaultSort());
 	m_solver->addAssertion(currentVariableExpression(_name) == value);
 }
+
+void SMTSolver::encodeVariableUpdateUnknown(const YulString& _name)
+{
+	if (m_variableSequenceCounter.count(_name))
+		++m_variableSequenceCounter[_name];
+	else
+		m_variableSequenceCounter[_name] = 1;
+
+	m_solver->newVariable(variableNameAtIndex(_name, m_variableSequenceCounter[_name]), defaultSort());
+	m_solver->addAssertion(0 <= currentVariableExpression(_name) && currentVariableExpression(_name) <= (bigint(1) << 256) - 1);
+}
diff --git a/libyul/optimiser/SMTSolver.h b/libyul/optimiser/SMTSolver.h
index bb37a1023..749c476e1 100644
--- a/libyul/optimiser/SMTSolver.h
+++ b/libyul/optimiser/SMTSolver.h
@@ -53,6 +53,7 @@ protected:
 	void encodeVariableDeclaration(VariableDeclaration const& _varDecl);
 	void encodeVariableAssignment(Assignment const& _assignment);
 	void encodeVariableUpdate(YulString const& _name, Expression const& _value);
+	void encodeVariableUpdateUnknown(YulString const& _name);
 
 	/// The encoding for a builtin. The type of encoding determines what we are
 	/// solving for.