disabling

HanielB · Feb 26, 2024 · 1d9ea6c · 1d9ea6c
1 parent bef410c
commit 1d9ea6c
Showing 1 changed file with 3 additions and 7 deletions.
diff --git a/test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2 b/test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2
@@ -1,16 +1,12 @@
 ; COMMAND-LINE: --ieval=use
 ; EXPECT: unsat
+;; Unary OR is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-const x9 Bool)
 (declare-fun p () Int)
 (declare-fun s4 (Int) Bool)
 (declare-fun s (Int) Bool)
 (declare-fun x (Int Int) Bool)
-(assert
-
-  (and (forall ((? Int)) (or (s p))) (forall ((q Int)) (not (x p q))) (forall ((q Int)) (or (x p q))) (forall ((? Int)) (or (s4 0) (s 0))) (or x9 (exists ((? Int)) (or (x 0 0))))))
-  (and (forall ((? Int)) (s p)) (forall ((q Int)) (not (x p q))) (forall ((q Int)) (x p q)) (forall ((? Int)) (or (s4 0) (s 0))) (or x9 (exists ((? Int)) (x 0 0))))
-
-
-
+(assert (and (forall ((? Int)) (or (s p))) (forall ((q Int)) (not (x p q))) (forall ((q Int)) (or (x p q))) (forall ((? Int)) (or (s4 0) (s 0))) (or x9 (exists ((? Int)) (or (x 0 0))))))
 (check-sat)