Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.x

20 files changed, 168 insertions, 68 deletions

diff --git a/config/.gitignore b/config/.gitignore
index dfeb8c222..c1e3d2423 100644
--- a/config/.gitignore
+++ b/config/.gitignore
@@ -9,3 +9,4 @@
 /missing
 /ltoptions.m4
 /install-sh
+/test-driver
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 721dedc70..65d46220b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -16,6 +16,7 @@
 
 #include <iostream>
 #include <fstream>
+#include <sstream>
 #include <iterator>
 #include <stdint.h>
 #include <cassert>
@@ -500,6 +501,14 @@ Expr Parser::nextExpression() throw(ParserException) {
   return result;
 }
 
+void Parser::attributeNotSupported(const std::string& attr) {
+  if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
+    stringstream ss;
+    ss << "warning: Attribute " << attr << " not supported (ignoring this and all following uses)";
+    d_input->warning(ss.str());
+    d_attributesWarnedAbout.insert(attr);
+  }
+}
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index fc956b463..958c8a5b5 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -144,6 +144,9 @@ class CVC4_PUBLIC Parser {
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
+  /** The set of attributes already warned about. */
+  std::set<std::string> d_attributesWarnedAbout;
+
   /**
    * The current set of unresolved types.  We can get by with this NOT
    * being on the scope, because we can only have one DATATYPE
@@ -451,6 +454,9 @@ public:
     d_input->warning(msg);
   }
 
+  /** Issue a warning to the user, but only once per attribute. */
+  void attributeNotSupported(const std::string& attr);
+
   /** Raise a parse error with the given message. */
   inline void parseError(const std::string& msg) throw(ParserException) {
     d_input->parseError(msg);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 87cf2083d..648666091 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -629,7 +629,7 @@ pattern[CVC4::Expr& expr]
     }
   ;
 
-simpleSymbolicExpr[CVC4::SExpr& sexpr]
+simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
 @declarations {
   CVC4::Kind k;
   std::string s;
@@ -647,6 +647,10 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
       ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
       sexpr = SExpr(ss.str());
     }
+  ;
+
+simpleSymbolicExpr[CVC4::SExpr& sexpr]
+  : simpleSymbolicExprNoKeyword[sexpr]
   | KEYWORD
     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
   ;
@@ -715,8 +719,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-  | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK 
-    {     
+  | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
+    {
       if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
         std::vector<CVC4::Expr> v;
         Expr e = f.getOperator();
@@ -928,22 +932,31 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
   Expr patexpr;
   std::vector<Expr> patexprs;
   Expr e2;
+  bool hasValue = false;
 }
-: KEYWORD
+  : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
   {
     attr = AntlrInput::tokenText($KEYWORD);
-    //EXPR_MANAGER->setNamedAttribute( expr, attr );
-    if( attr==":rewrite-rule" ){
-      //do nothing
-    } else if( attr==":axiom" || attr==":conjecture" ){
+    // EXPR_MANAGER->setNamedAttribute( expr, attr );
+    if(attr == ":rewrite-rule") {
+      if(hasValue) {
+        std::stringstream ss;
+        ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
+        PARSER_STATE->warning(ss.str());
+      }
+      // do nothing
+    } else if(attr == ":axiom" || attr == ":conjecture") {
+      if(hasValue) {
+        std::stringstream ss;
+        ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
+        PARSER_STATE->warning(ss.str());
+      }
       std::string attr_name = attr;
       attr_name.erase( attr_name.begin() );
       Command* c = new SetUserAttributeCommand( attr_name, expr );
       PARSER_STATE->preemptCommand(c);
     } else {
-      std::stringstream ss;
-      ss << "Attribute `" << attr << "' not supported";
-      PARSER_STATE->parseError(ss.str());
+      PARSER_STATE->attributeNotSupported(attr);
     }
   }
   | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); }  )+ RPAREN_TOK
@@ -951,6 +964,11 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       attr = std::string(":pattern");
       retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
     }
+  | ATTRIBUTE_NO_PATTERN_TOK LPAREN_TOK term[patexpr, e2]+ RPAREN_TOK
+    {
+      attr = std::string(":no-pattern");
+      PARSER_STATE->attributeNotSupported(attr);
+    }
   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
     {
       attr = std::string(":named");
@@ -1098,7 +1116,7 @@ quantOp[CVC4::Kind& kind]
 @init {
   Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : EXISTS_TOK      { $kind = CVC4::kind::EXISTS; }
+  : EXISTS_TOK    { $kind = CVC4::kind::EXISTS; }
   | FORALL_TOK    { $kind = CVC4::kind::FORALL; }
   ;
 
@@ -1374,6 +1392,7 @@ SIMPLIFY_TOK : 'simplify';
 
 // attributes
 ATTRIBUTE_PATTERN_TOK : ':pattern';
+ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
 ATTRIBUTE_NAMED_TOK : ':named';
 
 // operators (NOTE: theory symbols go here)
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f0a936c97..ecc224026 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -493,9 +493,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     case kind::BITVECTOR_UDIV:
       op << "BVUDIV";
       break;
+    case kind::BITVECTOR_UDIV_TOTAL:
+      op << "BVUDIV_TOTAL";
+      break;
     case kind::BITVECTOR_UREM:
       op << "BVUREM";
       break;
+    case kind::BITVECTOR_UREM_TOTAL:
+      op << "BVUREM_TOTAL";
+      break;
     case kind::BITVECTOR_SDIV:
       op << "BVSDIV";
       break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5985f38ef..5821fbc77 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -254,7 +254,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::BITVECTOR_SUB: out << "bvsub "; break;
   case kind::BITVECTOR_NEG: out << "bvneg "; break;
   case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
+  case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv_total "; break;
   case kind::BITVECTOR_UREM: out << "bvurem "; break;
+  case kind::BITVECTOR_UREM_TOTAL: out << "bvurem_total "; break;
   case kind::BITVECTOR_SDIV: out << "bvsdiv "; break;
   case kind::BITVECTOR_SREM: out << "bvsrem "; break;
   case kind::BITVECTOR_SMOD: out << "bvsmod "; break;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c82b7ca2c..77e43d518 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -631,6 +631,11 @@ void SmtEngine::finalOptionsAreSet() {
     }
   }
 
+  if(options::produceAssignments() && !options::produceModels()) {
+    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << std::endl;
+    setOption("produce-models", SExpr("true"));
+  }
+
   if(! d_logic.isLocked()) {
     // ensure that our heuristics are properly set up
     setLogicInternal();
@@ -2705,20 +2710,22 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
 
   vector<SExpr> sexprs;
   TypeNode boolType = d_nodeManager->booleanType();
+  TheoryModel* m = d_theoryEngine->getModel();
   for(AssignmentSet::const_iterator i = d_assignments->begin(),
         iend = d_assignments->end();
       i != iend;
       ++i) {
     Assert((*i).getType() == boolType);
 
-    // Normalize
-    Node n = Rewriter::rewrite(*i);
+    // Expand, then normalize
+    hash_map<Node, Node, NodeHashFunction> cache;
+    Node n = d_private->expandDefinitions(*i, cache);
+    n = Rewriter::rewrite(n);
 
     Trace("smt") << "--- getting value of " << n << endl;
-    TheoryModel* m = d_theoryEngine->getModel();
     Node resultNode;
-    if( m ){
-      resultNode = m->getValue( n );
+    if(m != NULL) {
+      resultNode = m->getValue(n);
     }
 
     // type-check the result we got
@@ -2727,12 +2734,12 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
     vector<SExpr> v;
     if((*i).getKind() == kind::APPLY) {
       Assert((*i).getNumChildren() == 0);
-      v.push_back((*i).getOperator().toString());
+      v.push_back(SExpr::Keyword((*i).getOperator().toString()));
     } else {
       Assert((*i).isVar());
-      v.push_back((*i).toString());
+      v.push_back(SExpr::Keyword((*i).toString()));
     }
-    v.push_back(resultNode.toString());
+    v.push_back(SExpr::Keyword(resultNode.toString()));
     sexprs.push_back(v);
   }
   return SExpr(sexprs);
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index fbf9a45ee..c25c40c22 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -648,6 +648,17 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 
   Bits r;
   uDivModRec(a, b, q, r, getSize(node)); 
+  // adding a special case for division by 0
+  std::vector<Node> iszero; 
+  for (unsigned i = 0; i < b.size(); ++i) {
+    iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); 
+  }
+  Node b_is_0 = utils::mkAnd(iszero); 
+  
+  for (unsigned i = 0; i < q.size(); ++i) {
+    q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]);
+    r[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), r[i]);
+  }
 
   // cache the remainder in case we need it later
   Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]);
@@ -664,6 +675,17 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
 
   Bits q;
   uDivModRec(a, b, q, rem, getSize(node)); 
+  // adding a special case for division by 0
+  std::vector<Node> iszero; 
+  for (unsigned i = 0; i < b.size(); ++i) {
+    iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); 
+  }
+  Node b_is_0 = utils::mkAnd(iszero); 
+  
+  for (unsigned i = 0; i < q.size(); ++i) {
+    q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]);
+    rem[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), rem[i]);
+  }
 
   // cache the quotient in case we need it later
   Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 8b080d104..498378638 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -207,7 +207,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a.unsignedDiv(b);
+  BitVector res = a.unsignedDivTotal(b);
   
   return utils::mkConst(res);
 }
@@ -222,7 +222,7 @@ Node RewriteRule<EvalUrem>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a.unsignedRem(b);
+  BitVector res = a.unsignedRemTotal(b);
   return utils::mkConst(res);
 }
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index e23d9deae..9da83ce41 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -45,7 +45,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
   d_selector_apps( c ),
   d_labels( c ),
-  d_conflict( c, false ){
+  d_conflict( c, false ),
+  d_collectTermsCache( c ){
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -758,31 +759,34 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
 
 
 void TheoryDatatypes::collectTerms( Node n ) {
-  for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-    collectTerms( n[i] );
-  }
-  if( n.getKind() == APPLY_CONSTRUCTOR ){
-    //we must take into account subterm relation when checking for cycles
+  if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
+    d_collectTermsCache[n] = true;
     for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-      Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl;
-      bool result = d_cycle_check.addEdgeNode( n, n[i] );
-      d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
+      collectTerms( n[i] );
     }
-  }else if( n.getKind() == APPLY_SELECTOR ){
-    if( d_selector_apps.find( n )==d_selector_apps.end() ){
-      d_selector_apps[n] = false;
-      //we must also record which selectors exist
-      Debug("datatypes") << "  Found selector " << n << endl;
-      if (n.getType().isBoolean()) {
-        d_equalityEngine.addTriggerPredicate( n );
-      }else{
-        d_equalityEngine.addTerm( n );
+    if( n.getKind() == APPLY_CONSTRUCTOR ){
+      //we must take into account subterm relation when checking for cycles
+      for( int i=0; i<(int)n.getNumChildren(); i++ ) {
+        Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl;
+        bool result = d_cycle_check.addEdgeNode( n, n[i] );
+        d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
       }
-      Node rep = getRepresentative( n[0] );
-      EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
-      if( !eqc->d_selectors ){
-        eqc->d_selectors = true;
-        instantiate( eqc, rep );
+    }else if( n.getKind() == APPLY_SELECTOR ){
+      if( d_selector_apps.find( n )==d_selector_apps.end() ){
+        d_selector_apps[n] = false;
+        //we must also record which selectors exist
+        Debug("datatypes") << "  Found selector " << n << endl;
+        if (n.getType().isBoolean()) {
+          d_equalityEngine.addTriggerPredicate( n );
+        }else{
+          d_equalityEngine.addTerm( n );
+        }
+        Node rep = getRepresentative( n[0] );
+        EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
+        if( !eqc->d_selectors ){
+          eqc->d_selectors = true;
+          instantiate( eqc, rep );
+        }
       }
     }
   }
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 90d82e255..9846e80f2 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -156,6 +156,8 @@ private:
   context::CDO<bool> d_conflict;
   /** The conflict node */
   Node d_conflictNode;
+  /** cache for which terms we have called collectTerms(...) on */
+  BoolMap d_collectTermsCache;
   /** pending assertions/merges */
   std::vector< Node > d_pending;
   std::map< Node, Node > d_pending_exp;
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 493a49e54..2f6dc47db 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -22,7 +22,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;

 using namespace CVC4::theory::quantifiers;

 

-void QuantifiersAttributes::setUserAttribute( std::string& attr, Node n ){

+void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){

   if( n.getKind()==FORALL ){

     if( attr=="axiom" ){

       Trace("quant-attr") << "Set axiom " << n << std::endl;

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 822d6c59f..88bac8bc9 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -40,7 +40,7 @@ struct QuantifiersAttributes
     *   This function will apply a custom set of attributes to all top-level universal

     *   quantifiers contained in n

     */

-  static void setUserAttribute( std::string& attr, Node n );

+  static void setUserAttribute( const std::string& attr, Node n );

 };

 

 

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index cfdb30f38..b1a7c9927 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -192,6 +192,6 @@ bool TheoryQuantifiers::restart(){
   }
 }
 
-void TheoryQuantifiers::setUserAttribute( std::string& attr, Node n ){
+void TheoryQuantifiers::setUserAttribute( const std::string& attr, Node n ){
   QuantifiersAttributes::setUserAttribute( attr, n );
 }
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index c3987144c..b4c8966c7 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -70,7 +70,7 @@ public:
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   bool flipDecision();
-  void setUserAttribute( std::string& attr, Node n );
+  void setUserAttribute( const std::string& attr, Node n );
   eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
 private:
   void assertUniversal( Node n );
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 2c178ec2e..4cbcba50e 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -178,23 +178,25 @@ public:
     Integer prod = d_value * y.d_value;
     return BitVector(d_size, prod);
   }
-  
-  BitVector unsignedDiv (const BitVector& y) const {
+  /** 
+   * Total division function that returns 0 when the denominator is 0.  
+   */
+  BitVector unsignedDivTotal (const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
-    // TODO: decide whether we really want these semantics
     if (y.d_value == 0) {
-      return BitVector(d_size, Integer(0));
+      return BitVector(d_size, 0u);
     }
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value > 0, y);
     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
   }
-
-  BitVector unsignedRem(const BitVector& y) const {
+  /** 
+   * Total division function that returns 0 when the denominator is 0.  
+   */
+  BitVector unsignedRemTotal(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
-    // TODO: decide whether we really want these semantics
     if (y.d_value == 0) {
-      return BitVector(d_size, d_value);
+      return BitVector(d_size, 0u);
     }
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value > 0, y);
diff --git a/test/Makefile.am b/test/Makefile.am
index 014aecc43..6cccca05c 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -15,7 +15,7 @@ units systemtests regress regress0 regress1 regress2 regress3:
 test: check
 
 am__tty_colors = \
-red=; grn=; lgn=; blu=; std=; \
+red=; grn=; lgn=; blu=; mag=; std=; \
 test "X$(AM_COLOR_TESTS)" != Xno \
 && test "X$$TERM" != Xdumb \
 && { test "X$(AM_COLOR_TESTS)" = Xalways || test -t 1 2>/dev/null; } \
@@ -24,6 +24,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \
   grn=''; \
   lgn=''; \
   blu=''; \
+  mag=''; \
   std=''; \
 }
 
@@ -61,14 +62,23 @@ check-recursive: check-pre
 check-pre:
 	@rm -f $(subdirs_to_check:=/test-suite.log)
 
+if HAVE_CXXTESTGEN
+HANDLE_UNIT_TEST_SUMMARY = \
+	if test -s "unit/test-suite.log"; then :; else \
+		echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \
+	fi
+else
+HANDLE_UNIT_TEST_SUMMARY = \
+	echo "$${mag}Unit tests not supported, since CxxTest wasn't found$$std"; \
+	rm -f "unit/test-suite.log"
+endif
+
 if AUTOMAKE_1_11
 # automake 1.11 version
 check-local:
 	@$(am__tty_colors); \
 	echo $${blu}===============================  TESTING SUMMARY  =============================$$std; \
-	if test -s "unit/test-suite.log"; then :; else \
-		echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \
-	fi; \
+	$(HANDLE_UNIT_TEST_SUMMARY); \
 	if test -s "system/test-suite.log"; then :; else \
 		echo "$${red}System tests did not run; maybe there were compilation problems ?$$std"; \
 	fi; \
@@ -90,9 +100,7 @@ else
 check-local:
 	@$(am__tty_colors); \
 	echo $${blu}===============================  TESTING SUMMARY  =============================$$std; \
-	if test -s "unit/test-suite.log"; then :; else \
-		echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \
-	fi; \
+	$(HANDLE_UNIT_TEST_SUMMARY); \
 	if test -s "system/test-suite.log"; then :; else \
 		echo "$${red}System tests did not run; maybe there were compilation problems ?$$std"; \
 	fi; \
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 0f6c11be9..3b30a8d9e 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -142,7 +142,8 @@ BUG_TESTS = \
 	bug411.smt2 \
 	bug421.smt2 \
 	bug421b.smt2 \
-	bug425.cvc
+	bug425.cvc \
+	bug480.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug480.smt2 b/test/regress/regress0/bug480.smt2
new file mode 100644
index 000000000..ba58f354b
--- /dev/null
+++ b/test/regress/regress0/bug480.smt2
@@ -0,0 +1,11 @@
+; EXPECT: sat
+; EXPECT: ((foo true) (bar false) (baz true))
+; EXIT: 10
+(set-logic QF_LIA)
+(set-option :produce-assignments true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (! (or (! (= x (+ y 5)) :named foo) (! (= x (- y 5)) :named bar)) :named baz))
+(assert (and (> x 0) (<= y 5)))
+(check-sat)
+(get-assignment)
diff --git a/test/unit/no_cxxtest b/test/unit/no_cxxtest
index cf8b8d729..57e5064d9 100755
--- a/test/unit/no_cxxtest
+++ b/test/unit/no_cxxtest
@@ -3,10 +3,10 @@
 echo
 echo '***************************************************************************'
 echo '*                                                                         *'
-echo '*  ERROR:  CxxTest was not found at configure-time; tests cannot be run.  *'
+echo '*   WARNING:  CxxTest not found at configure time; tests cannot be run.   *'
 echo '*                                                                         *'
 echo '***************************************************************************'
 echo
 
-exit 1
-
+# skip this test, rather than reporting an error
+exit 77