From 6aba5bcee7c8aaee57ee1dbfb0e03712e5a9e291 Mon Sep 17 00:00:00 2001 From: someplaceguy Date: Fri, 26 Jan 2024 02:37:46 +0000 Subject: [PATCH] HolSmt: remove duplicate self-tests These test cases are already being tested above in the `num` section. --- src/HolSmt/selftest.sml | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml index 6a501bfcca..e4b72bedaa 100644 --- a/src/HolSmt/selftest.sml +++ b/src/HolSmt/selftest.sml @@ -548,11 +548,6 @@ in (``(x:real) < x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(x:real) < y ==> 42 * x < 42 * y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), - (``0n <= 1n``, [thm_AUTO, thm_YO]), - (``1n <= 0n``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), - (``(x:num) <= x``, [thm_AUTO, thm_YO]), - (``(x:num) <= y ==> 2 * x <= 2 * y``, [thm_AUTO, thm_YO]), - (``1r > 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), (``0r > 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(x:real) > x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),