From 5c1ecce2a321639f29495763876b11d387926db9 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Wed, 1 Jun 2022 22:16:16 +0200
Subject: [PATCH] Implement inner xor.

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

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 866f4a1c4..db1abd6f1 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -844,6 +844,11 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi
 			state().clauses.emplace_back(Clause{vector<Literal>{_left, negate(a), negate(b)}});
 			state().clauses.emplace_back(Clause{vector<Literal>{_left, a, b}});
 		}
+		else if (_right.name == "xor")
+		{
+			solAssert(_right.arguments.size() == 2);
+			addBooleanEquality(negate(_left), _right.arguments.at(0) == _right.arguments.at(1), move(_letBindings));
+		}
 		else
 			solAssert(false, "Unsupported operation: " + _right.name);
 	}