From 44d5edd7bf00f7b288b3ea84d19e3d81b375c3e1 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Tue, 25 Jun 2024 18:31:44 +0200
Subject: [PATCH] [test] Updated CVC5 tests
---
tests/cvc5.t | 45 ---------------------------------------------
1 file changed, 45 deletions(-)
diff --git a/tests/cvc5.t b/tests/cvc5.t
index ce6c0a6..2bbd58f 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))
--
GitLab