diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 17a093236..87f02be42 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -242,14 +242,16 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
 		addAssertion(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1);
 	else if (_expr.name == ">")
 		addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0));
+	else
+		cout << "Unknown operator " << _expr.name << endl;
 }
 
 
 pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> const& _expressionsToEvaluate)
 {
-	cout << "Solving boolean constraint system" << endl;
-	cout << toString() << endl;
-	cout << "--------------" << endl;
+//	cout << "Solving boolean constraint system" << endl;
+//	cout << toString() << endl;
+//	cout << "--------------" << endl;
 
 	if (m_state.back().infeasible)
 		return make_pair(CheckResult::UNSATISFIABLE, vector<string>{});
@@ -330,6 +332,8 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
 				Literal::PositiveVariable,
 				m_state.back().variables.at(_expr.name)
 			};
+		else
+			cout << "cannot encode " << _expr.name << " - not a boolean literal variable." << endl;
 	}
 	else if (_expr.name == "not")
 		return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)));
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index 9f4c08efd..853c8d413 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -165,7 +165,7 @@ void ReasoningBasedSimplifier::operator()(If& _if)
 
 	if (bodyTerminates)
 	{
-		cout << "Body always terminates." << endl;
+		//cout << "Body always terminates." << endl;
 		if (isBoolean(*_if.condition))
 			m_solver->addAssertion(!cond);
 		else
@@ -267,10 +267,28 @@ void ReasoningBasedSimplifier::handleDeclaration(
 	}
 	//case evmasm::Instruction::MUL:
 		// TODO encode constants?
-	//case evmasm::Instruction::DIV:
+	case evmasm::Instruction::DIV:
+		m_solver->addAssertion(variable <= *x);
+		break;
 	case evmasm::Instruction::ADDMOD:
 		m_solver->addAssertion(variable < *z);
 		break;
+	case evmasm::Instruction::SHL:
+		if (holds_alternative<Literal>(_arguments.at(0)))
+		{
+			u256 shiftAmount = valueOfLiteral(get<Literal>(_arguments.at(0)));
+			cout << "shift by " << shiftAmount << endl;
+		}
+		break;
+	case evmasm::Instruction::SHR:
+		if (holds_alternative<Literal>(_arguments.at(0)))
+		{
+			u256 shiftAmount = valueOfLiteral(get<Literal>(_arguments.at(0)));
+			cout << "shift by " << shiftAmount << endl;
+		}
+		break;
+	case evmasm::Instruction::SAR:
+		break;
 	case evmasm::Instruction::LT:
 		m_solver->addAssertion(variable == (*x < *y));
 		break;
@@ -281,7 +299,12 @@ void ReasoningBasedSimplifier::handleDeclaration(
 	//	case evmasm::Instruction::SGT:
 	// TODO
 	case evmasm::Instruction::EQ:
-		m_solver->addAssertion(variable == (*x == *y));
+		if (isBoolean(_arguments.at(0)) == isBoolean(_arguments.at(1)))
+			m_solver->addAssertion(variable == (*x == *y));
+		else if (isBoolean(_arguments.at(0)))
+			m_solver->addAssertion(variable == ((*x && *y >= 1) || (!*x && *y == 0)));
+		else
+			m_solver->addAssertion(variable == ((*y && *x >= 1) || (!*y && *x == 0)));
 		break;
 	case evmasm::Instruction::ISZERO:
 		if (isBoolean(_arguments.at(0)))
@@ -313,6 +336,7 @@ void ReasoningBasedSimplifier::handleDeclaration(
 		break;
 	// TODO all builtins whose return values can be restricted.
 	default:
+		cout << "Not handling instruction " << evmasm::instructionInfo(_instruction).name << endl;
 		break;
 	}
 }