From a9a2fe4949ed047117a1e116d24bcfb022f0881e Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Tue, 15 Feb 2011 21:39:45 +0000
Subject: Workaround bug in Z3 SMT parser

---
 Binaries/UnivBackPred2.smt2          | 8 ++++----
 Source/Provers/SMTLib/SMTLibNamer.cs | 3 ++-
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2
index 1cfe5356..33c82099 100644
--- a/Binaries/UnivBackPred2.smt2
+++ b/Binaries/UnivBackPred2.smt2
@@ -5,10 +5,10 @@
 (set-logic UFNIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "industrial")
-(declare-sort T@U 0)
-(declare-sort T@T 0)
+(declare-sort |T@U| 0)
+(declare-sort |T@T| 0)
 (declare-fun int_div (Int Int) Int)
 (declare-fun int_mod (Int Int) Int)
-(declare-fun UOrdering2 (T@U T@U) Bool)
-(declare-fun UOrdering3 (T@T T@U T@U) Bool)
+(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
+(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)
 
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index e57d8deb..3de2e81d 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -9,7 +9,8 @@ namespace Microsoft.Boogie.SMTLib
   public class SMTLibNamer : UniqueNamer
   {
     // The following Boogie ID characters are not SMT ID characters: `'\#
-    const string idCharacters = "~!@$%^&*_-+=<>.?/";
+    // Accomodate Z3 SMT2 lexer bug - it doesn't like @ and such in identifiers    
+    const string idCharacters = "_"; // "~!@$%^&*_-+=<>.?/";    
 
 
     static string[] reservedSmtWordsList = 
-- 
cgit v1.2.3