more disabling

test/regress/cli/regress1/quantifiers/dd.bug812-ieval.smt2

@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --enum-inst --ieval=use
 ; EXPECT: unsat
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-fun p (Int) Int)
 (declare-fun H (Int Int Int) Int)

test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2

@@ -1,14 +1,16 @@
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
-(declare-fun a () Real)   
-(assert 
-    (and  
-        (and 
-            (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real)) 
-            (or  (and  (and  (and (and (< (+ (+ (+ 0.0 (* 68.0 ?c)) 0.0) (* 33.0 a)) 0.0) (<= 0.0 2.0)) 
+(declare-fun a () Real)
+(assert
+    (and
+        (and
+            (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real))
+            (or  (and  (and  (and (and (< (+ (+ (+ 0.0 (* 68.0 ?c)) 0.0) (* 33.0 a)) 0.0) (<= 0.0 2.0))
             (or (<= 0.0 (+  (*  (+ (* 55.0 ?d) 0.0) (* 49.0 ?b)) 0.0))))))))))
         )
     )
-) 
+)
 
 (check-sat)

test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2

@@ -1,5 +1,7 @@
 ; COMMAND-LINE: -i
 ; EXPECT: unsat
+;; Unary OR is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (push)
 (assert (or (forall ((v Real)) (or (exists ((V Real)) (or (exists ((V Real)) (= 0 (mod (to_int v) (to_int (- v)))))))))))

test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2

@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --sygus-inst
 ; EXPECT: unsat
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (assert (and (forall ((v (Array (_ BitVec 1) Bool))) (select v (_ bv0 1)))))
 (check-sat)