diff options
| -rw-r--r-- | Binaries/UnivBackPred2.smt2 | 8 | ||||
| -rw-r--r-- | 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 =
|