From bbac4aa2161970562eec470d0fc1eaac930f0edc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= <arpl@cs.stanford.edu>
Date: Tue, 5 Nov 2024 22:49:52 -0800
Subject: [PATCH] Remove non-compliant characters from symbol names

---
 frontends/btor2_encoder.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/frontends/btor2_encoder.cpp b/frontends/btor2_encoder.cpp
index 6087a2f1..d2f230ff 100644
--- a/frontends/btor2_encoder.cpp
+++ b/frontends/btor2_encoder.cpp
@@ -19,6 +19,7 @@
 #include "btor2_encoder.h"
 #include "utils/logger.h"
 
+#include <cstddef>
 #include <iostream>
 #include "assert.h"
 
@@ -289,6 +290,13 @@ void BTOR2Encoder::parse(const std::string filename)
     if (l_->tag == BTOR2_TAG_state) {
       if (l_->symbol) {
         symbol_ = l_->symbol;
+        // The characters | and \ are not allowed in any SMT-LIB symbol.
+        for (auto ch : {'|', '\\'}) {
+          std::size_t pos;
+          while((pos = symbol_.find(ch)) != symbol_.npos) {
+            symbol_.replace(pos, 1, "_");
+          }
+        }
       } else {
         auto renaming_lookup_pos = state_renaming_table.find(l_->id);
         if (renaming_lookup_pos != state_renaming_table.end() )