1 files changed, 0 insertions, 54 deletions
diff --git a/examples/SimpleVC.tcl b/examples/SimpleVC.tcl
deleted file mode 100755
index 4e1c76c5a..000000000
--- a/examples/SimpleVC.tcl
+++ /dev/null
@@ -1,54 +0,0 @@
-#! /usr/bin/tclsh
-##! \file SimpleVC.tcl
-### \verbatim
-### Original author: mdeters
-### Major contributors: none
-### Minor contributors (to current version): none
-### This file is part of the CVC4 prototype.
-### Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
-### Courant Institute of Mathematical Sciences
-### New York University
-### See the file COPYING in the top-level source directory for licensing
-### information.\endverbatim
-###
-### \brief A simple demonstration of the Tcl interface
-###
-### A simple demonstration of the Tcl interface.  Compare to the
-### C++ interface in simple_vc_cxx.cpp; they are quite similar.
-###
-### To run, use something like:
-###
-###   ln -s ../builds/src/bindings/tcl/.libs/CVC4.so CVC4.so
-###   ./SimpleVC.tcl
-####
-
-load CVC4.so CVC4
-
-ExprManager em
-SmtEngine smt em
-
-# Prove that for integers x and y:
-#   x > 0 AND y > 0  =>  2x + y >= 3
-
-set integer [ExprManager_integerType em]
-
-set x [ExprManager_mkVar em "x" $integer]
-set y [ExprManager_mkVar em "y" $integer]
-set zero [ExprManager_mkConst em [Integer _ 0]]
-
-set x_positive [ExprManager_mkExpr em $GT $x $zero]
-set y_positive [ExprManager_mkExpr em $GT $y $zero]
-
-set two [ExprManager_mkConst em [Integer _ 2]]
-set twox [ExprManager_mkExpr em $MULT $two $x]
-set twox_plus_y [ExprManager_mkExpr em $PLUS $twox $y]
-
-set three [ExprManager_mkConst em [Integer _ 3]]
-set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three]
-
-set formula [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]]
-
-puts "Checking entailment of formula [Expr_toString $formula] with CVC4."
-puts "CVC4 should report ENTAILED."
-puts "Result from CVC4 is: [Result_toString [SmtEngine_checkEntailed smt $formula]]"
-