diff options
author | MichalMoskal <unknown> | 2011-02-15 21:39:45 +0000 |
---|---|---|
committer | MichalMoskal <unknown> | 2011-02-15 21:39:45 +0000 |
commit | a9a2fe4949ed047117a1e116d24bcfb022f0881e (patch) | |
tree | 2983c52938bb75bd3629602f36fad2dd7aee1e21 /Binaries | |
parent | 12d606d7f90455d263150175b47a9c87a99ef4c1 (diff) |
Workaround bug in Z3 SMT parser
Diffstat (limited to 'Binaries')
-rw-r--r-- | Binaries/UnivBackPred2.smt2 | 8 |
1 files changed, 4 insertions, 4 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)
|