From faa3a242ee375005a4a6ca6e7557426585997d29 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Mon, 30 May 2022 18:17:16 +0200
Subject: [PATCH] Support some xor.

---
 libsolutil/BooleanLP.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 090bf7b78..55f27acc9 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -318,6 +318,12 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, LetBindi
 			literals.emplace_back(parseLiteralOrReturnEqualBoolean(arg, _letBindings));
 		state().clauses.emplace_back(Clause{move(literals)});
 	}
+	else if (_expr.name == "xor")
+	{
+		solAssert(_expr.arguments.size() == 2);
+		addAssertion(_expr.arguments.at(0) || _expr.arguments.at(1));
+		addAssertion(!_expr.arguments.at(0) || !_expr.arguments.at(1));
+	}
 	else if (_expr.name == "not")
 	{
 		solAssert(_expr.arguments.size() == 1);