diff --git a/tests/cvc5.t b/tests/cvc5.t
index ce6c0a686b5d60a552f1dcff0411520ad7c95d1a..2bbd58f5d600325afdff585b0a1407ad9885f558 100644
--- a/tests/cvc5.t
+++ b/tests/cvc5.t
@@ -31,51 +31,6 @@ Test verify
   ;;; SMT-LIB2: real arithmetic
   (define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
   (define-fun fp.isIntegral64 ((x Float64)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
-  ;; "add_div"
-  (assert
-    (forall ((x Real) (y Real) (z Real))
-      (=> (not (= z 0.0)) (= (/ (+ x y) z) (+ (/ x z) (/ y z))))))
-  
-  ;; "sub_div"
-  (assert
-    (forall ((x Real) (y Real) (z Real))
-      (=> (not (= z 0.0)) (= (/ (- x y) z) (- (/ x z) (/ y z))))))
-  
-  ;; "neg_div"
-  (assert
-    (forall ((x Real) (y Real))
-      (=> (not (= y 0.0)) (= (/ (- x) y) (- (/ x y))))))
-  
-  ;; "assoc_mul_div"
-  (assert
-    (forall ((x Real) (y Real) (z Real))
-      (=> (not (= z 0.0)) (= (/ (* x y) z) (* x (/ y z))))))
-  
-  ;; "assoc_div_mul"
-  (assert
-    (forall ((x Real) (y Real) (z Real))
-      (=>
-        (and (not (= y 0.0)) (not (= z 0.0)))
-        (= (/ (/ x y) z) (/ x (* y z))))))
-  
-  ;; "assoc_div_div"
-  (assert
-    (forall ((x Real) (y Real) (z Real))
-      (=>
-        (and (not (= y 0.0)) (not (= z 0.0)))
-        (= (/ x (/ y z)) (/ (* x z) y)))))
-  
-  ;; "CompatOrderMult"
-  (assert
-    (forall ((x Real) (y Real) (z Real))
-      (=> (<= x y) (=> (<= 0.0 z) (<= (* x z) (* y z))))))
-  
-  ;; "max_real"
-  (declare-fun max_real () Real)
-  
-  ;; "max_int"
-  (declare-fun max_int () Int)
-  
   ;; "sqr"
   (define-fun sqr ((x Real)) Real
     (* x x))