[test] Updated CVC5 tests

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))