compat layer cleanup

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 6db6b440ee9b1abd68b0da46045f182ca736523d..7b748a2d3098f2c116ae5ccd0adc1b9af4209d54 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -680,6 +680,7 @@ ValidityChecker::ValidityChecker() :
   setUpOptions(d_options, *d_clflags);
   d_em = new CVC4::ExprManager(d_options);
   d_smt = new CVC4::SmtEngine(d_em);
+  d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
 }
 
 ValidityChecker::ValidityChecker(const CLFlags& clflags) :
@@ -688,9 +689,11 @@ ValidityChecker::ValidityChecker(const CLFlags& clflags) :
   setUpOptions(d_options, *d_clflags);
   d_em = new CVC4::ExprManager(d_options);
   d_smt = new CVC4::SmtEngine(d_em);
+  d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
 }
 
 ValidityChecker::~ValidityChecker() {
+  delete d_parserContext;
   delete d_clflags;
 }
 
@@ -948,11 +951,11 @@ Type ValidityChecker::intType() {
 }
 
 Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Subranges not supported by CVC4 yet (sorry!)");
 }
 
 Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)");
 }
 
 Type ValidityChecker::tupleType(const Type& type0, const Type& type1) {
@@ -977,23 +980,23 @@ Type ValidityChecker::tupleType(const std::vector<Type>& types) {
 }
 
 Type ValidityChecker::recordType(const std::string& field, const Type& type) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Type ValidityChecker::recordType(const std::string& field0, const Type& type0,
                                  const std::string& field1, const Type& type1) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Type ValidityChecker::recordType(const std::string& field0, const Type& type0,
                                  const std::string& field1, const Type& type1,
                                  const std::string& field2, const Type& type2) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Type ValidityChecker::recordType(const std::vector<std::string>& fields,
                                  const std::vector<Type>& types) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Type ValidityChecker::dataType(const std::string& name,
@@ -1042,11 +1045,11 @@ Type ValidityChecker::createType(const std::string& typeName) {
 }
 
 Type ValidityChecker::createType(const std::string& typeName, const Type& def) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  d_parserContext->defineType(typeName, def);
 }
 
 Type ValidityChecker::lookupType(const std::string& typeName) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  return d_parserContext->getSort(typeName);
 }
 
 ExprManager* ValidityChecker::getEM() {
@@ -1054,16 +1057,17 @@ ExprManager* ValidityChecker::getEM() {
 }
 
 Expr ValidityChecker::varExpr(const std::string& name, const Type& type) {
-  return d_em->mkVar(name, type);
+  return d_parserContext->mkVar(name, type);
 }
 
 Expr ValidityChecker::varExpr(const std::string& name, const Type& type,
                               const Expr& def) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  FatalAssert(def.getType() == type, "expected types to match");
+  d_parserContext->defineVar(name, def);
 }
 
 Expr ValidityChecker::lookupVar(const std::string& name, Type* type) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  return d_parserContext->getVariable(name);
 }
 
 Type ValidityChecker::getType(const Expr& e) {
@@ -1138,7 +1142,7 @@ void ValidityChecker::printExpr(const Expr& e, std::ostream& os) {
 }
 
 Expr ValidityChecker::parseExpr(const Expr& e) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  return e;
 }
 
 Type ValidityChecker::parseType(const Expr& e) {
@@ -1167,14 +1171,11 @@ Expr ValidityChecker::exprFromString(const std::string& s, InputLanguage lang) {
   }
 
   CVC4::parser::Parser* p = CVC4::parser::ParserBuilder(d_em, "<internal>").withStringInput(s).withInputLanguage(lang).build();
-  Expr dummy = p->nextExpression();
-  if( dummy.isNull() ) {
+  p->useDeclarationsFrom(d_parserContext);
+  Expr e = p->nextExpression();
+  if( e.isNull() ) {
     throw CVC4::parser::ParserException("Parser result is null: '" + s + "'");
   }
-  //DebugAssert(dummy.getKind() == RAW_LIST, "Expected list expression");
-  //DebugAssert(dummy.arity() == 2, "Expected two children");
-
-  Expr e = parseExpr(dummy[1]);
 
   delete p;
 
@@ -1237,7 +1238,7 @@ Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) {
 }
 
 Op ValidityChecker::createOp(const std::string& name, const Type& type) {
-  return d_em->mkVar(name, type);
+  return d_parserContext->mkVar(name, type);
 }
 
 Op ValidityChecker::createOp(const std::string& name, const Type& type,
@@ -1246,7 +1247,9 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type,
 }
 
 Op ValidityChecker::lookupOp(const std::string& name, Type* type) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Op op = d_parserContext->getFunction(name);
+  *type = op.getType();
+  return op;
 }
 
 Expr ValidityChecker::funExpr(const Op& op, const Expr& child) {
@@ -1333,32 +1336,32 @@ Expr ValidityChecker::geExpr(const Expr& left, const Expr& right) {
 }
 
 Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0,
                                  const std::string& field1, const Expr& expr1) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0,
                                  const std::string& field1, const Expr& expr1,
                                  const std::string& field2, const Expr& expr2) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields,
                                  const std::vector<Expr>& exprs) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field,
                                     const Expr& newValue) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Records not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::readExpr(const Expr& array, const Expr& index) {
@@ -1657,12 +1660,12 @@ Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) {
 }
 
 Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Tuples not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index,
                                       const Expr& newValue) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Tuples not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) {
@@ -1679,50 +1682,50 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp
 
 Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& uid,
                                    const Type& type) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body,
                                  const Expr& trigger) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body,
                                  const std::vector<Expr>& triggers) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body,
                                  const std::vector<std::vector<Expr> >& triggers) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 void ValidityChecker::setTriggers(const Expr& e, const std::vector<std::vector<Expr> > & triggers) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 void ValidityChecker::setTriggers(const Expr& e, const std::vector<Expr>& triggers) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 void ValidityChecker::setTrigger(const Expr& e, const Expr& trigger) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 void ValidityChecker::setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 Expr ValidityChecker::existsExpr(const std::vector<Expr>& vars, const Expr& body) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
 }
 
 Op ValidityChecker::lambdaExpr(const std::vector<Expr>& vars, const Expr& body) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  Unimplemented("Lambda expressions not supported by CVC4 yet (sorry!)");
 }
 
 Op ValidityChecker::transClosure(const Op& op) {
@@ -1951,9 +1954,10 @@ void ValidityChecker::loadFile(const std::string& fileName,
   opts.interactive = interactive;
   opts.interactiveSetByUser = true;
   CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts);
-  CVC4::parser::Parser* parser = parserBuilder.build();
-  doCommands(parser, d_smt, opts);
-  delete parser;
+  CVC4::parser::Parser* p = parserBuilder.build();
+  p->useDeclarationsFrom(d_parserContext);
+  doCommands(p, d_smt, opts);
+  delete p;
 }
 
 void ValidityChecker::loadFile(std::istream& is,
@@ -1964,9 +1968,11 @@ void ValidityChecker::loadFile(std::istream& is,
   opts.interactive = interactive;
   opts.interactiveSetByUser = true;
   CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts);
-  CVC4::parser::Parser* parser = parserBuilder.withStreamInput(is).build();
-  doCommands(parser, d_smt, opts);
-  delete parser;
+  CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build();
+  d_parserContext = p;
+  p->useDeclarationsFrom(d_parserContext);
+  doCommands(p, d_smt, opts);
+  delete p;
 }
 
 Statistics& ValidityChecker::getStatistics() {

diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index b4c9cba3ed9048d5c9d7105029d1e18495eb3e7a..1e4511ba51586bbab57c663182921f8601a9ef08 100644 (file)
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -60,6 +60,8 @@
 #include "util/exception.h"
 #include "util/hash.h"
 
+#include "parser/parser.h"
+
 #include <stdlib.h>
 #include <map>
 #include <utility>
@@ -462,6 +464,7 @@ class CVC4_PUBLIC ValidityChecker {
   CVC4::Options d_options;
   CVC4::ExprManager* d_em;
   CVC4::SmtEngine* d_smt;
+  CVC4::parser::Parser* d_parserContext;
 
   ValidityChecker(const CLFlags& clflags);
 

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 46544559a229c8b43c88a2ccd74c5882887db450..70bd45c31a132d966ea693a1b847c5cff0928e80 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -473,7 +473,8 @@ public:
    * This feature is useful when e.g. reading out-of-band expression data:
    * 1. Parsing --replay log files produced with --replay-log.
    * 2. Perhaps a multi-query benchmark file is being single-stepped
-   *    with intervening queries on stdin that must reference
+   *    with intervening queries on stdin that must reference the same
+   *    declaration scope(s).
    *
    * However, the feature must be used carefully.  Pushes and pops
    * should be performed with the correct current declaration scope.

diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp
index ecf664923f22ab84a5aec2cc5bf1e4c2f9abb627..d86526da8429e5a12c99064e668ff8a4811473bf 100644 (file)
--- a/test/system/cvc3_main.cpp
+++ b/test/system/cvc3_main.cpp
@@ -124,7 +124,7 @@ void test ()
      Expr f2 = vc->funExpr(f, e);
      Expr f3 = vc->funExpr(f, f2);
 
-     DebugAssert(e != f2 && e != f3, "Refcount problems");
+     FatalAssert(e != f2 && e != f3, "Refcount problems");
 
      Expr x (vc->boundVarExpr ("x", "0", it));//x0:int
      vector<Expr> xs;
@@ -160,11 +160,11 @@ void test1()
   try {
 
     IF_DEBUG(bool b =) check(vc, vc->trueExpr());
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     vc->push();
     IF_DEBUG(b =) check(vc, vc->falseExpr());
-    DebugAssert(!b, "Should be invalid");
+    FatalAssert(!b, "Should be invalid");
     vc->pop();          
 
     // Check p OR ~p
@@ -173,7 +173,7 @@ void test1()
     Expr e = vc->orExpr(p, vc->notExpr(p));
 
     IF_DEBUG(b =) check(vc, e);
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     // Check x = y -> f(x) = f(y)
 
@@ -187,7 +187,7 @@ void test1()
 
     e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(fx, fy));
     IF_DEBUG(b =) check(vc, e);
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     // Check f(x) = f(y) -> x = y
 
@@ -195,7 +195,7 @@ void test1()
     IF_DEBUG(int scopeLevel = vc->scopeLevel();)
     vc->push();
     IF_DEBUG(b =) check(vc, e);
-    DebugAssert(!b, "Should be invalid");
+    FatalAssert(!b, "Should be invalid");
 
     // Get counter-example
     
@@ -211,7 +211,7 @@ void test1()
     // Reset to initial scope
     cout << "Resetting" << endl;
     vc->pop();
-    DebugAssert(scopeLevel == vc->scopeLevel(), "scope error");
+    FatalAssert(scopeLevel == vc->scopeLevel(), "scope error");
     cout << "Scope level: " << vc->scopeLevel() << endl << endl;
 
     // Check w = x & x = y & y = z & f(x) = f(y) & x = 1 & z = 2
@@ -231,7 +231,7 @@ void test1()
     cout << endl << "simplify(w) = ";
     vc->printExpr(vc->simplify(w));
     cout << endl;
-    DebugAssert(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1");
+    FatalAssert(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1");
 
     newAssertion(vc, vc->eqExpr(z, vc->ratExpr(2)));
     assertions.clear();
@@ -247,7 +247,7 @@ void test1()
     
     cout << "simplify(w) = ";
     vc->printExpr(vc->simplify(w));
-    DebugAssert(vc->simplify(w)==w, "Expected simplify(w) = w");
+    FatalAssert(vc->simplify(w)==w, "Expected simplify(w) = w");
     cout << endl;
     
     assertions.clear();
@@ -275,10 +275,10 @@ void test2()
     vc->assertFormula(c.eqExpr(vc->ratExpr(0)) || c.eqExpr(vc->ratExpr(1)));
 
     IF_DEBUG(bool b =) check(vc, vc->leExpr(bexpr, vc->ratExpr(10)));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     IF_DEBUG(b =) check(vc, vc->falseExpr());
-    DebugAssert(!b, "Should be invalid");
+    FatalAssert(!b, "Should be invalid");
     vc->returnFromCheck();
 
     // Check x = y -> g(x,y) = g(y,x)
@@ -299,7 +299,7 @@ void test2()
 
     Expr e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(gxy, gyx));
     IF_DEBUG(b =) check(vc, e);
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     Op h = vc->createOp("h", realxreal2real);
 
@@ -308,7 +308,7 @@ void test2()
 
     e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(hxy, hyx));
     IF_DEBUG(b =) check(vc, e);
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
   } catch(const Exception& e) {
     exitStatus = 1;
@@ -803,7 +803,7 @@ void test8() {
     Expr witness;
     try {
       Type t = vc->subtypeType(lambda, witness);
-      DebugAssert(false, "Typechecking exception expected");
+      FatalAssert(false, "Typechecking exception expected");
     } catch(const TypecheckException&) {
       // fall through
     }
@@ -1063,14 +1063,14 @@ void test11()
     cout << "Assert x = y" << endl;
     vc->assertFormula(xeqy);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==3,"Implied literal error 0");
+    FatalAssert(c==3,"Implied literal error 0");
 
     cout << "Push" << endl;
     vc->push();
     cout << "Assert x /= z" << endl;
     vc->assertFormula(!xeqz);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==4,"Implied literal error 1");
+    FatalAssert(c==4,"Implied literal error 1");
     cout << "Pop" << endl;
     vc->pop();
 
@@ -1079,7 +1079,7 @@ void test11()
     cout << "Assert y /= z" << endl;
     vc->assertFormula(!yeqz);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==4,"Implied literal error 2");
+    FatalAssert(c==4,"Implied literal error 2");
     cout << "Pop" << endl;
     vc->pop();
 
@@ -1088,7 +1088,7 @@ void test11()
     cout << "Assert p(x)" << endl;
     vc->assertFormula(px);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==2,"Implied literal error 3");
+    FatalAssert(c==2,"Implied literal error 3");
     cout << "Pop" << endl;
     vc->pop();
 
@@ -1097,7 +1097,7 @@ void test11()
     cout << "Assert p(y)" << endl;
     vc->assertFormula(py);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==2,"Implied literal error 4");
+    FatalAssert(c==2,"Implied literal error 4");
     cout << "Pop" << endl;
     vc->pop();
 
@@ -1109,7 +1109,7 @@ void test11()
     cout << "Assert y = x" << endl;
     vc->assertFormula(yeqx);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==3,"Implied literal error 5");
+    FatalAssert(c==3,"Implied literal error 5");
     cout << "Pop" << endl;
     vc->pop();
 
@@ -1118,11 +1118,11 @@ void test11()
     cout << "Assert p(x)" << endl;
     vc->assertFormula(px);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==1,"Implied literal error 6");
+    FatalAssert(c==1,"Implied literal error 6");
     cout << "Assert x = y" << endl;
     vc->assertFormula(xeqy);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==4,"Implied literal error 7");
+    FatalAssert(c==4,"Implied literal error 7");
     cout << "Pop" << endl;
     vc->pop();
 
@@ -1131,11 +1131,11 @@ void test11()
     cout << "Assert NOT p(x)" << endl;
     vc->assertFormula(!px);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==1,"Implied literal error 8");
+    FatalAssert(c==1,"Implied literal error 8");
     cout << "Assert x = y" << endl;
     vc->assertFormula(xeqy);
     c = printImpliedLiterals(vc);
-    DebugAssert(c==4,"Implied literal error 9");
+    FatalAssert(c==4,"Implied literal error 9");
     cout << "Pop" << endl;
     vc->pop();
 
@@ -1160,8 +1160,8 @@ void test12()
     Expr exprObj_trueID = vc->trueExpr();
     Expr exprObj_falseID = vc->notExpr(vc->trueExpr());
     vc->popto(initial_layer);
-    DebugAssert(vc->scopeLevel() == initial_scope, "Expected no change");
-    DebugAssert(vc->stackLevel() == initial_layer, "Expected no change");
+    FatalAssert(vc->scopeLevel() == initial_scope, "Expected no change");
+    FatalAssert(vc->stackLevel() == initial_layer, "Expected no change");
     // TODO: what happens if we push and then popscope?
   } catch(const Exception& e) {
     exitStatus = 1;
@@ -1380,7 +1380,7 @@ void test16()  {
     cout << "Scope level: " << vc->scopeLevel() << endl;
     cout << "Counter-example:" << endl;
     vc->getCounterExample(assertions);
-    DebugAssert(assertions.size() > 0, "Expected non-empty counter-example");
+    FatalAssert(assertions.size() > 0, "Expected non-empty counter-example");
     for (unsigned i = 0; i < assertions.size(); ++i) {
       vc->printExpr(assertions[i]);
     }
@@ -1396,7 +1396,7 @@ void test16()  {
       for(; it!= end; it++) {
        Expr eq;
        if(it->first.getType().isBool()) {
-         DebugAssert((it->second).isBoolConst(),
+         FatalAssert((it->second).isBoolConst(),
                      "Bad variable assignement: e = "+(it->first).toString()
                      +"\n\n val = "+(it->second).toString());
          if((it->second).isTrue())
@@ -1431,7 +1431,7 @@ void test17()  {
       types.push_back(vc->stringExpr("list"));
 
       Type badList = vc->dataType("list", "cons", selectors, types);
-      DebugAssert(false, "Typechecking exception expected");
+      FatalAssert(false, "Typechecking exception expected");
     } catch(const TypecheckException&) {
       // fall through
     }
@@ -1461,7 +1461,7 @@ void test17()  {
 
       Expr sel = vc->datatypeSelExpr("car", cons);
       IF_DEBUG(bool b =) check(vc, vc->eqExpr(sel, x));
-      DebugAssert(b, "Should be valid");
+      FatalAssert(b, "Should be valid");
 
     }
     delete vc;
@@ -1494,7 +1494,7 @@ void test17()  {
       types[0][0].push_back(vc->stringExpr("list1"));
 
       vc->dataType(names, constructors, selectors, types, returnTypes);
-      DebugAssert(false, "Typechecking exception expected");
+      FatalAssert(false, "Typechecking exception expected");
     } catch(const TypecheckException&) {
       // fall through
     }
@@ -1553,7 +1553,7 @@ void test17()  {
       Expr cons1_2 = vc->datatypeConsExpr("cons1", args);
 
       IF_DEBUG(bool b =) check(vc, vc->impliesExpr(hyp, vc->eqExpr(z, cons1_2)));
-      DebugAssert(b, "Should be valid");
+      FatalAssert(b, "Should be valid");
 
     }
     delete vc;
@@ -1578,7 +1578,7 @@ void test17()  {
       args.push_back(!vc->eqExpr(x,z));
 
       IF_DEBUG(bool b =) check(vc, !vc->andExpr(args));
-      DebugAssert(b, "Should be valid");
+      FatalAssert(b, "Should be valid");
 
     }
   } catch(const Exception& e) {
@@ -1648,7 +1648,7 @@ void test18()
     vc->push();
     try {
       check(vc, vc->notExpr(vc->eqExpr(zero, null)));
-      DebugAssert(false, "Should have caught tcc exception");
+      FatalAssert(false, "Should have caught tcc exception");
     } catch(const TypecheckException&) { }
 
     vc->pop();
@@ -1658,16 +1658,16 @@ void test18()
     vc->push();
     try {
       check(vc, spxeqx);
-      DebugAssert(false, "Should have caught tcc exception");
+      FatalAssert(false, "Should have caught tcc exception");
     } catch(const TypecheckException&) { }
 
     vc->pop();
     bool b = check(vc, vc->impliesExpr(vc->datatypeTestExpr("succ", x), spxeqx));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     b = check(vc, vc->orExpr(vc->datatypeTestExpr("zero", x),
                              vc->datatypeTestExpr("succ", x)));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     Expr y = vc->varExpr("y", nat);
     Expr xeqy = vc->eqExpr(x, y);
@@ -1679,16 +1679,16 @@ void test18()
     Expr sy = vc->datatypeConsExpr("succ", args);
     Expr sxeqsy = vc->eqExpr(sx,sy);
     b = check(vc, vc->impliesExpr(xeqy, sxeqsy));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     b = check(vc, vc->notExpr(vc->eqExpr(sx, zero)));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     b = check(vc, vc->impliesExpr(sxeqsy, xeqy));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     b = check(vc, vc->notExpr(vc->eqExpr(sx, x)));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
   } catch(const Exception& e) {
     exitStatus = 1;
@@ -1737,7 +1737,7 @@ void test19()
   
     IF_DEBUG(bool Succ =) vc->query(Q);
 
-    DebugAssert(Succ, "Expected valid formula");
+    FatalAssert(Succ, "Expected valid formula");
 
   } catch(const Exception& e) {
     exitStatus = 1;
@@ -1788,7 +1788,7 @@ void test20()  {
 
     vc->dataType(names, constructors, selectors, types, returnTypes);
 
-    DebugAssert(returnTypes[0].card() == CARD_FINITE, "Expected finite");
+    FatalAssert(returnTypes[0].card() == CARD_FINITE, "Expected finite");
     Unsigned size = returnTypes[0].sizeFinite();
     Unsigned i = 0;
     for (; i < size; ++i) {
@@ -1814,32 +1814,32 @@ void test21()  {
     Expr x2 = vc->exprFromString("x");
     cout << "x1: " << x1;
     cout << "\nx2: " << x2;
-    DebugAssert(x1 == x2, "Expected x1 == x2");
+    FatalAssert(x1 == x2, "Expected x1 == x2");
 
     Expr y1 = vc->varExpr("y",t);
     Expr y2 = vc->exprFromString("y");
     cout << "\ny1: " << y1;
     cout << "\ny2: " << y2;
-    DebugAssert(y1 == y2, "Expected y1 == y2");
+    FatalAssert(y1 == y2, "Expected y1 == y2");
 
     Expr a1 = vc->gtExpr(x1,vc->ratExpr(0,1));
     Expr a2 = vc->exprFromString("x > 0");
     cout << "\na1: " << a1;
     cout << "\na2: " << a2;
-    DebugAssert(a1 == a2, "Expected a1 == a2");
+    FatalAssert(a1 == a2, "Expected a1 == a2");
 
     Expr b1 = vc->ltExpr(x1,y1);
     Expr b2 = vc->exprFromString ("x < y");
     cout << "\nb1: " << b1;
     cout << "\nb2: " << b2;
-    DebugAssert(b1 == b2, "Expected b1 == b2");
+    FatalAssert(b1 == b2, "Expected b1 == b2");
 
     Expr e1 = a1 && b1;
     Expr e2 = vc->exprFromString("x > 0 AND x < y");
 
     cout << "\ne1: " << e1;
     cout << "\ne2: " << e2;
-    DebugAssert(e1 == e2, "Expected e1 == e2");
+    FatalAssert(e1 == e2, "Expected e1 == e2");
   } catch(const Exception& e) {
     exitStatus = 1;
     cout << "*** Exception caught in test21(): \n" << e << endl;
@@ -1867,56 +1867,56 @@ void test22() {
     patternvv.push_back(patternv);
 
     vc->setTriggers(p,patternv);
-    DebugAssert( eqExprVecVecs(p.getTriggers(), patternvv),
+    FatalAssert( eqExprVecVecs(p.getTriggers(), patternvv),
                  "Expected p.getTriggers() == patternvv: " + p.toString() );
 
     vc->setTriggers(p,patternvv);
 
-    DebugAssert( eqExprVecVecs(p.getTriggers(), patternvv),
+    FatalAssert( eqExprVecVecs(p.getTriggers(), patternvv),
                  "Expected p.getTriggers() == patternvv: " + p.toString() );
 
     // [chris 10/4/2009] Not sure why, but this fails
 
     // Expr q(vc->exprFromString("FORALL (x:INT) : PATTERN (f(x)) : x < f(x)"));
 
-    // DebugAssert( eqExprVecVecs(q.getTriggers(), patternvv),
+    // FatalAssert( eqExprVecVecs(q.getTriggers(), patternvv),
     //              "Expected q.getTriggers() == patternvv"  + q.toString());
 
     vector<Expr> vars;
     vars.push_back(x);
     Expr r(vc->forallExpr( vars, vc->ltExpr(x,fx), patternvv ));
 
-    DebugAssert( eqExprVecVecs(r.getTriggers(), patternvv),
+    FatalAssert( eqExprVecVecs(r.getTriggers(), patternvv),
                  "Expected r.getTriggers() == patternvv: " + r.toString() );
 
     Expr s(vc->exprFromString("FORALL (x:INT) : x > f(x)"));
     vc->setTrigger(s,fx);
     
     std::vector<std::vector<Expr> > trigsvv = s.getTriggers();
-    DebugAssert( trigsvv.size() == 1, 
+    FatalAssert( trigsvv.size() == 1, 
                  "Expected s.getTriggers().size() == 1: " + trigsvv.size() );
 
     std::vector<Expr> trigsv = trigsvv[0];
-    DebugAssert( trigsv.size() == 1, 
+    FatalAssert( trigsv.size() == 1, 
                  "Expected s.getTriggers()[0].size() == 1: "
                  + trigsv.size() );
 
-    DebugAssert( trigsv[0] == fx, 
+    FatalAssert( trigsv[0] == fx, 
                  "Expected s.getTriggers()[0][0] == fx: "
                  + (trigsv[0].toString()) );
 
     Expr t(vc->exprFromString("FORALL (x:INT) : x > f(x)"));
     vc->setMultiTrigger(t,patternv);
     trigsvv = t.getTriggers();
-    DebugAssert( trigsvv.size() == 1,
+    FatalAssert( trigsvv.size() == 1,
                  "Expected t.getTriggers().size() == 1: " + trigsvv.size() );
 
     trigsv = trigsvv[0];
-    DebugAssert( trigsv.size() == 1,
+    FatalAssert( trigsv.size() == 1,
                  "Expected t.getTriggers()[0].size() == 1: "
                  + trigsv.size() );
 
-    DebugAssert( trigsv[0] == fx,
+    FatalAssert( trigsv[0] == fx,
                  "Expected t.getTriggers()[0][0] == fx: "
                  + (trigsv[0].toString()) );
   } catch(const Exception& e) {
@@ -1953,7 +1953,7 @@ void test23() {
     Expr u(s.substExpr(oldExprs,newExprs));
     cout << "u=" << u << "\n";
 
-    DebugAssert( t == u, "Expected t==u" );
+    FatalAssert( t == u, "Expected t==u" );
   } catch(const Exception& e) {
     exitStatus = 1;
     cout << "*** Exception caught in test23(): \n" << e << endl;
@@ -1978,19 +1978,19 @@ void test24() {
     cout << p  << "\n";
 
     vector<vector<Expr> > pTriggers(p.getTriggers());
-    DebugAssert( pTriggers.size() == 1, 
+    FatalAssert( pTriggers.size() == 1, 
                  "Expected one trigger set. Found: " + 
                  int2string(pTriggers.size()));
-    DebugAssert( pTriggers[0].size() == 1, 
+    FatalAssert( pTriggers[0].size() == 1, 
                  "Expected one trigger. Found: " +
                  int2string( pTriggers[0].size()));
     /* We can't check that the trigger == ax, because x will have
      * been replaced with a bvar
      */
-    DebugAssert( pTriggers[0][0].getKind() == READ,
+    FatalAssert( pTriggers[0][0].getKind() == READ,
                  "Expected READ expression. Found: " +
                  pTriggers[0][0].getKind());
-    DebugAssert( pTriggers[0][0][0] == a,
+    FatalAssert( pTriggers[0][0][0] == a,
                  "Expected read on array: " + a.toString() +
                  "\nFound: " + pTriggers[0][0][0].toString() );
 
@@ -2005,16 +2005,16 @@ void test24() {
     cout << q << "\n";
 
     vector<vector<Expr> > qTriggers(q.getTriggers());
-    DebugAssert( qTriggers.size() == 1, 
+    FatalAssert( qTriggers.size() == 1, 
                  "Expected one trigger set. Found: " + 
                  int2string(qTriggers.size()));
-    DebugAssert( qTriggers[0].size() == 1, 
+    FatalAssert( qTriggers[0].size() == 1, 
                  "Expected one trigger. Found: " +
                  int2string( qTriggers[0].size()));
-    DebugAssert( qTriggers[0][0].getKind() == READ,
+    FatalAssert( qTriggers[0][0].getKind() == READ,
                  "Expected READ expression. Found: " +
                  qTriggers[0][0].getKind());
-    DebugAssert( qTriggers[0][0][0] == aPrime,
+    FatalAssert( qTriggers[0][0][0] == aPrime,
                  "Expected read on array: " + aPrime.toString() +
                  "\nFound: " + qTriggers[0][0][0].toString() );
   } catch(const Exception& e) {
@@ -2041,7 +2041,7 @@ void test25() {
     Expr w = vc->ratExpr(-1,10);
     cout << "-1 over 10 (ints): " << w << endl;
 
-    DebugAssert(x == y && y == z && z == w, "Error in rational constants");
+    FatalAssert(x == y && y == z && z == w, "Error in rational constants");
 
   } catch(const Exception& e) {
     exitStatus = 1;
@@ -2063,17 +2063,17 @@ void test26() {
     Expr e2 = vc->newBVSHL(x, vc->newBVConstExpr(16, 32));
 
     bool b = check(vc, vc->eqExpr(e1, e2));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     e1 = vc->newFixedRightShiftExpr(x, 16);
     e2 = vc->newBVLSHR(x, vc->newBVConstExpr(16, 32));
 
     b = check(vc, vc->eqExpr(e1, e2));
-    DebugAssert(b, "Should be valid");
+    FatalAssert(b, "Should be valid");
 
     e2 = vc->newBVASHR(x, vc->newBVConstExpr(16, 32));
     b = check(vc, vc->eqExpr(e1, e2));
-    DebugAssert(!b, "Should be invalid");
+    FatalAssert(!b, "Should be invalid");
 
   } catch(const Exception& e) {
     exitStatus = 1;