1 files changed, 0 insertions, 62 deletions
diff --git a/examples/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp
deleted file mode 100644
index 8986aaeca..000000000
--- a/examples/simple_vc_compat_cxx.cpp
+++ /dev/null
@@ -1,62 +0,0 @@
-/*********************                                                        */
-/*! \file simple_vc_compat_cxx.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A simple demonstration of the C++ compatibility interface
- ** (quite similar to the old CVC3 C++ interface)
- **
- ** A simple demonstration of the C++ compatibility interface (quite
- ** similar to the old CVC3 C++ interface).  Note that the library is
- ** named "libcvc4compat," to mark it as being part of CVC4, but the
- ** header file is "cvc3_compat.h" to indicate the similarity to the
- ** CVC3 interface, and the namespace is "CVC3".  CVC3::Expr and
- ** CVC4::Expr are incompatible; to avoid confusion, it is best to not
- ** include both the CVC3 and CVC4 interface headers.
- **/
-
-#include <iostream>
-
-// #include <cvc4/compat/cvc3_compat.h> // use this after CVC4 is properly installed
-#include "compat/cvc3_compat.h"
-
-using namespace std;
-using namespace CVC3;
-
-int main() {
-  ValidityChecker* vc = ValidityChecker::create();
-
-  // Prove that for integers x and y:
-  //   x > 0 AND y > 0  =>  2x + y >= 3
-
-  Type integer = vc->intType();
-
-  Expr x = vc->varExpr("x", integer);
-  Expr y = vc->varExpr("y", integer);
-  Expr zero = vc->ratExpr(0);
-
-  Expr x_positive = vc->gtExpr(x, zero);
-  Expr y_positive = vc->gtExpr(y, zero);
-
-  Expr two = vc->ratExpr(2);
-  Expr twox = vc->multExpr(two, x);
-  Expr twox_plus_y = vc->plusExpr(twox, y);
-
-  Expr three = vc->ratExpr(3);
-  Expr twox_plus_y_geq_3 = vc->geExpr(twox_plus_y, three);
-
-  Expr formula = vc->impliesExpr(vc->andExpr(x_positive, y_positive),
-                                twox_plus_y_geq_3);
-
-  cout << "Checking validity of formula " << formula << " with CVC4." << endl;
-  cout << "CVC4 should report VALID." << endl;
-  cout << "Result from CVC4 is: " << vc->query(formula) << endl;
-
-  return 0;
-}