6 files changed, 0 insertions, 143 deletions

diff --git a/math/Makefile b/math/Makefile
index c1f1e6716618..7468ef19ff71 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -40,7 +40,6 @@
     SUBDIR += convertall
     SUBDIR += coq
     SUBDIR += cvc3
-    SUBDIR += cvcl
     SUBDIR += cxsc
     SUBDIR += dcdflib
     SUBDIR += diehard
diff --git a/math/cvcl/Makefile b/math/cvcl/Makefile
deleted file mode 100644
index 1b431bf3b343..000000000000
--- a/math/cvcl/Makefile
+++ /dev/null
@@ -1,39 +0,0 @@
-# New ports collection makefile for:	cvcl
-# Date created:		2006-09-15
-# Whom:			Li-wen Hsu <lwhsu@lwhsu.org>
-#
-# $FreeBSD$
-#
-
-PORTNAME=	cvcl
-PORTVERSION=	2.5.1
-CATEGORIES=	math
-MASTER_SITES=	http://www.cs.nyu.edu/acsys/cvcl/download/
-
-MAINTAINER=	lwhsu@FreeBSD.org
-COMMENT=	An automatic theorem prover for the SMT problem
-
-LIB_DEPENDS=	gmp:${PORTSDIR}/math/libgmp4
-
-DEPRECATED=	CVC Lite is no longer supported. Please use CVC3 (math/cvc3) for all your validity checking needs!
-EXPIRATION_DATE=	2007-06-30
-
-CONFIGURE_ARGS=	--with-arith=gmp \
-		--with-extra-libs=${LOCALBASE}/lib \
-		--with-extra-includes=${LOCALBASE}/include \
-		--with-build=optimized
-CXXFLAGS+=	-fPIC
-GNU_CONFIGURE=	yes
-USE_BISON=	yes
-USE_GMAKE=	yes
-USE_LDCONFIG=	yes
-
-WRKSRC=		${WRKDIR}/cvcl-20060527
-
-.include <bsd.port.pre.mk>
-
-.if ${OSVERSION} >= 700042
-BROKEN=	Broken with gcc 4.2
-.endif
-
-.include <bsd.port.post.mk>
diff --git a/math/cvcl/distinfo b/math/cvcl/distinfo
deleted file mode 100644
index 9a40b76b9e6a..000000000000
--- a/math/cvcl/distinfo
+++ /dev/null
@@ -1,3 +0,0 @@
-MD5 (cvcl-2.5.1.tar.gz) = c41afb57e90438efa6e7360e330039f4
-SHA256 (cvcl-2.5.1.tar.gz) = a1a008816c170f3ddea6f513c6bbf11ed10f155b55431284ebad97dd26e61772
-SIZE (cvcl-2.5.1.tar.gz) = 689957
diff --git a/math/cvcl/files/patch-configure b/math/cvcl/files/patch-configure
deleted file mode 100644
index 4b87c64d4d6f..000000000000
--- a/math/cvcl/files/patch-configure
+++ /dev/null
@@ -1,11 +0,0 @@
---- configure.orig	Sat May 27 13:23:58 2006
-+++ configure	Wed Sep 27 11:52:11 2006
-@@ -1371,7 +1371,7 @@
- 
- 
- RUN_TESTS_OPTIONS=""
--CXXFLAGS=""
-+#CXXFLAGS=""
- 
- 
- # Check whether --with-build or --without-build was given.
diff --git a/math/cvcl/pkg-descr b/math/cvcl/pkg-descr
deleted file mode 100644
index bd68d695f4d1..000000000000
--- a/math/cvcl/pkg-descr
+++ /dev/null
@@ -1,8 +0,0 @@
-CVC Lite is an automatic theorem prover for the Satisfiability Modulo
-Theories (SMT) problem. Its features include: support for a variety of
-theories; interactive as well as C and C++ library interfaces; proof and
-model generation abilities; predicate subtyping; and suppport for quantifiers.
-In addition, there are essentially no limits on its use for research or
-commercial purposes (see license).
-
-WWW:	http://www.cs.nyu.edu/acsys/cvcl/
diff --git a/math/cvcl/pkg-plist b/math/cvcl/pkg-plist
deleted file mode 100644
index c82a2d7aa313..000000000000
--- a/math/cvcl/pkg-plist
+++ /dev/null
@@ -1,81 +0,0 @@
-bin/cvcl
-include/cvcl/assumptions.h
-include/cvcl/assumptions_value.h
-include/cvcl/c_interface.h
-include/cvcl/c_interface_defs.h
-include/cvcl/cdflags.h
-include/cvcl/cdlist.h
-include/cvcl/cdmap.h
-include/cvcl/cdmap_ordered.h
-include/cvcl/cdo.h
-include/cvcl/circuit.h
-include/cvcl/clause.h
-include/cvcl/cnf.h
-include/cvcl/cnf_manager.h
-include/cvcl/command_line_exception.h
-include/cvcl/command_line_flags.h
-include/cvcl/common_proof_rules.h
-include/cvcl/compat_hash_map.h
-include/cvcl/compat_hash_set.h
-include/cvcl/context.h
-include/cvcl/cvclutil.h
-include/cvcl/debug.h
-include/cvcl/dpllt.h
-include/cvcl/dpllt_basic.h
-include/cvcl/eval_exception.h
-include/cvcl/exception.h
-include/cvcl/expr.h
-include/cvcl/expr_hash.h
-include/cvcl/expr_manager.h
-include/cvcl/expr_map.h
-include/cvcl/expr_op.h
-include/cvcl/expr_stream.h
-include/cvcl/expr_transform.h
-include/cvcl/expr_value.h
-include/cvcl/fdstream.h
-include/cvcl/kinds.h
-include/cvcl/lang.h
-include/cvcl/memory_manager.h
-include/cvcl/memory_manager_chunks.h
-include/cvcl/memory_manager_malloc.h
-include/cvcl/notifylist.h
-include/cvcl/parser.h
-include/cvcl/proof.h
-include/cvcl/rational.h
-include/cvcl/parser_exception.h
-include/cvcl/pretty_printer.h
-include/cvcl/queryresult.h
-include/cvcl/sat_api.h
-include/cvcl/search.h
-include/cvcl/search_impl_base.h
-include/cvcl/search_sat.h
-include/cvcl/search_simple.h
-include/cvcl/search_fast.h
-include/cvcl/smartcdo.h
-include/cvcl/smtlib_exception.h
-include/cvcl/sound_exception.h
-include/cvcl/statistics.h
-include/cvcl/theorem.h
-include/cvcl/theorem_manager.h
-include/cvcl/theorem_producer.h
-include/cvcl/theory_arith.h
-include/cvcl/theory_array.h
-include/cvcl/theory_bitvector.h
-include/cvcl/theory_core.h
-include/cvcl/type.h
-include/cvcl/theory_datatype.h
-include/cvcl/theory_datatype_lazy.h
-include/cvcl/theory.h
-include/cvcl/theory_quant.h
-include/cvcl/theory_records.h
-include/cvcl/theory_simulate.h
-include/cvcl/theory_uf.h
-include/cvcl/translator.h
-include/cvcl/typecheck_exception.h
-include/cvcl/variable.h
-include/cvcl/vc_cmd.h
-include/cvcl/vc.h
-include/cvcl/vcl.h
-lib/libcvclite.a
-lib/libcvclite.so
-@dirrm include/cvcl