summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2011-02-15 21:39:45 +0000
committerGravatar MichalMoskal <unknown>2011-02-15 21:39:45 +0000
commita9a2fe4949ed047117a1e116d24bcfb022f0881e (patch)
tree2983c52938bb75bd3629602f36fad2dd7aee1e21 /Binaries
parent12d606d7f90455d263150175b47a9c87a99ef4c1 (diff)
Workaround bug in Z3 SMT parser
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/UnivBackPred2.smt28
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)