fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug217.smt2 as regressions; fix to build system to only run regressions (not units) if you "make -C test regress", for example (this matches behavior elsewhere)

1 files changed, 6 insertions, 5 deletions

diff --git a/src/util/result.h b/src/util/result.h
index 62ddc74d0..1e0729332 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -60,6 +60,7 @@ public:
     INCOMPLETE,
     TIMEOUT,
     MEMOUT,
+    NO_STATUS,
     OTHER,
     UNKNOWN_REASON
   };
@@ -132,16 +133,16 @@ public:
     return d_unknownExplanation;
   }
 
-  bool operator==(const Result& r) const;
-  inline bool operator!=(const Result& r) const;
-  Result asSatisfiabilityResult() const;
-  Result asValidityResult() const;
+  bool operator==(const Result& r) const throw();
+  inline bool operator!=(const Result& r) const throw();
+  Result asSatisfiabilityResult() const throw();
+  Result asValidityResult() const throw();
 
   std::string toString() const;
 
 };/* class Result */
 
-inline bool Result::operator!=(const Result& r) const {
+inline bool Result::operator!=(const Result& r) const throw() {
   return !(*this == r);
 }