From 4ff7a4dc4a1022aa0f94acabeb81def4a5cbf02d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 23 Sep 2015 15:22:48 +0200
Subject: [PATCH] Don't give invalid characters to the solver
---
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index f82df1a3b..275013666 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -111,7 +111,9 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
protected val library = program.library
- protected def id2sym(id: Identifier): SSymbol = SSymbol(id.uniqueNameDelimited("!"))
+ protected def id2sym(id: Identifier): SSymbol = {
+ SSymbol(id.uniqueNameDelimited("!").replace("|", "$pipe").replace("\\", "$backslash"))
+ }
protected def freshSym(id: Identifier): SSymbol = freshSym(id.name)
protected def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
--
GitLab