ITE context is mostly bad. Now disabled by default.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1331 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/unit_test/ite.smt2 b/unit_test/ite.smt2
deleted file mode 100644 (file)
index ae7f809..0000000
--- a/unit_test/ite.smt2
+++ /dev/null
@@ -1,42 +0,0 @@
-
-(set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
-(set-info :category "check")
-(set-info :status sat)
-
-; These can be simplified by considering the context
-; of the ITES they contain. 
-
-(declare-fun a () Bool)
-(declare-fun b () Bool)
-(declare-fun c () Bool)
-(assert (ite (or a b) (not (or a b)) c ) )
-
-(declare-fun d () Bool)
-(declare-fun e () Bool)
-(assert (ite (and e d) e (and e d)  ) )
-
-(declare-fun f () Bool)
-(declare-fun g () Bool)
-(declare-fun h () Bool)
-(assert (ite (or f g) (and g f)  g   ) )
-
-(declare-fun i () Bool)
-(declare-fun j () Bool)
-(declare-fun k () Bool)
-(assert (ite i (ite j i (not i)) i ))
-
-; This doesn't simplify nicely down yet::
-;  108:(OR 
-;  50:m
-;   52:(AND 
-;     48:l
-;     50:m))
-(declare-fun l () Bool)
-(declare-fun m () Bool)
-(assert (ite (not (and l m)) m l  ) )
-
-
-(check-sat)
-(exit)
-