summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
authorGravatar Peter Collingbourne <peter@pcc.me.uk>2012-09-06 20:33:21 +0100
committerGravatar Peter Collingbourne <peter@pcc.me.uk>2012-09-06 20:33:21 +0100
commit85a65323bda16d372a9e163dc4225e5d5535d14c (patch)
tree6e4999e040de5a5c7511521939c576957509b538 /Binaries
parentf369261b5b9953380d8fb8e0f7b020167482a491 (diff)
Implement support for alternative SMT solvers -- CVC3 and CVC4
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/UnivBackPred2.smt22
1 files changed, 0 insertions, 2 deletions
diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2
index 97c052c9..d3e3777f 100644
--- a/Binaries/UnivBackPred2.smt2
+++ b/Binaries/UnivBackPred2.smt2
@@ -7,5 +7,3 @@
(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 tickleBool (Bool) Bool)
-(assert (and (tickleBool true) (tickleBool false)))