From 4101c67cba9b3d8554728c48a29c3a4d67d7e515 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Fri, 11 Aug 2023 21:39:51 +0200
Subject: [PATCH] Update to let inlining

---
 libsmtutil/CHCSmtLib2Interface.cpp | 77 +++++++++++++++---------------
 1 file changed, 38 insertions(+), 39 deletions(-)

diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index b84ba2750..0ccbd3cb1 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -484,8 +484,8 @@ namespace
 		SMTLib2Expression & operator[](std::string const& varName)
 		{
 			auto it = bindings.find(varName);
-			assert(it != bindings.end());
-			assert(!it->second.empty());
+			solAssert(it != bindings.end());
+			solAssert(!it->second.empty());
 			return it->second.back();
 		}
 
@@ -529,47 +529,46 @@ namespace
 			auto const& atom = asAtom(expr);
 			if (bindings.has(atom))
 				expr = bindings[atom];
+			return;
 		}
-		else
+		auto& subexprs = asSubExpressions(expr);
+		solAssert(!subexprs.empty());
+		auto const& first = subexprs.at(0);
+		if (isAtom(first) && asAtom(first) == "let")
 		{
-			auto& subexprs = asSubExpressions(expr);
-			assert(!subexprs.empty());
-			auto const& first = subexprs.at(0);
-			if (isAtom(first) && asAtom(first) == "let")
+			solAssert(subexprs.size() >= 3);
+			solAssert(!isAtom(subexprs[1]));
+			auto& bindingExpressions = asSubExpressions(subexprs[1]);
+			// process new bindings
+			std::vector<std::pair<std::string, SMTLib2Expression>> newBindings;
+			for (auto& binding: bindingExpressions)
 			{
-				solAssert(!isAtom(subexprs[1]));
-				auto& bindingExpressions = asSubExpressions(subexprs[1]);
-				// process new bindings
-				std::vector<std::pair<std::string, SMTLib2Expression>> newBindings;
-				for (auto& binding: bindingExpressions)
-				{
-					solAssert(!isAtom(binding));
-					auto& bindingPair = asSubExpressions(binding);
-					solAssert(bindingPair.size() == 2);
-					solAssert(isAtom(bindingPair.at(0)));
-					inlineLetExpressions(bindingPair.at(1), bindings);
-					newBindings.emplace_back(asAtom(bindingPair.at(0)), bindingPair.at(1));
-				}
-				bindings.pushScope();
-				for (auto&& [name, expr] : newBindings)
-					bindings.addBinding(std::move(name), std::move(expr));
-				newBindings.clear();
-
-				// get new subexpression
-				inlineLetExpressions(subexprs.at(2), bindings);
-				// remove the new bindings
-				bindings.popScope();
-
-				// update the expression
-				auto tmp = std::move(subexprs.at(2));
-				expr = std::move(tmp);
-				return;
-			}
-			// not a let expression, just process all arguments
-			for (auto& subexpr: subexprs)
-			{
-				inlineLetExpressions(subexpr, bindings);
+				solAssert(!isAtom(binding));
+				auto& bindingPair = asSubExpressions(binding);
+				solAssert(bindingPair.size() == 2);
+				solAssert(isAtom(bindingPair.at(0)));
+				inlineLetExpressions(bindingPair.at(1), bindings);
+				newBindings.emplace_back(asAtom(bindingPair.at(0)), bindingPair.at(1));
 			}
+			bindings.pushScope();
+			for (auto&& [name, expr]: newBindings)
+				bindings.addBinding(std::move(name), std::move(expr));
+			newBindings.clear();
+
+			// get new subexpression
+			inlineLetExpressions(subexprs.at(2), bindings);
+			// remove the new bindings
+			bindings.popScope();
+
+			// update the expression
+			auto tmp = std::move(subexprs.at(2));
+			expr = std::move(tmp);
+			return;
+		}
+		// not a let expression, just process all arguments
+		for (auto& subexpr: subexprs)
+		{
+			inlineLetExpressions(subexpr, bindings);
 		}
 	}