fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug217...

diff --git a/Makefile.subdir b/Makefile.subdir
index 4b3afdbbf8f749490ce9861451cc10a13c3615b8..293b2771b60164175452a71c4a009739f2480450 100644 (file)
--- a/Makefile.subdir
+++ b/Makefile.subdir
@@ -21,8 +21,8 @@ all %:
 .PHONY: check units
 ifeq ($(srcdir:test/%=test),test)
 # under the test/ directory, additional subtargets
-.PHONY: regress0 regress1 regress2 regress3
-check units regress0 regress1 regress2 regress3:
+.PHONY: regress regress0 regress1 regress2 regress3
+check units regress regress0 regress1 regress2 regress3:
        @if test -e $(builddir); then \
                echo cd $(builddir); \
                cd $(builddir); \
@@ -49,5 +49,5 @@ check units:
 endif
 
 # synonyms for "check"
-.PHONY: regress test
-regress test: check
+.PHONY: test
+test: check

diff --git a/src/util/result.cpp b/src/util/result.cpp
index b8f34f47f003682d75c469b7f46cacfd34d63dcc..9760eaefbcb4cffd323b067253e623c14e73fc84 100644 (file)
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -47,9 +47,6 @@ Result::Result(const string& instr) :
   } else if(s == "invalid") {
     d_which = TYPE_VALIDITY;
     d_validity = INVALID;
-  } else if(s == "unknown") {
-    d_which = TYPE_SAT;
-    d_sat = SAT_UNKNOWN;
   } else if(s == "incomplete") {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
@@ -62,13 +59,16 @@ Result::Result(const string& instr) :
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = MEMOUT;
+  } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
+    d_which = TYPE_SAT;
+    d_sat = SAT_UNKNOWN;
   } else {
     IllegalArgument(s, "expected satisfiability/validity result, "
                     "instead got `%s'", s.c_str());
   }
 }
 
-bool Result::operator==(const Result& r) const {
+bool Result::operator==(const Result& r) const throw() {
   if(d_which != r.d_which) {
     return false;
   }
@@ -85,50 +85,56 @@ bool Result::operator==(const Result& r) const {
   return false;
 }
 
-Result Result::asSatisfiabilityResult() const {
+Result Result::asSatisfiabilityResult() const throw() {
   if(d_which == TYPE_SAT) {
     return *this;
   }
 
-  Assert(d_which == TYPE_VALIDITY);
-
-  switch(d_validity) {
+  if(d_which == TYPE_VALIDITY) {
+    switch(d_validity) {
 
-  case INVALID:
-    return Result(SAT);
+    case INVALID:
+      return Result(SAT);
 
-  case VALID:
-    return Result(UNSAT);
+    case VALID:
+      return Result(UNSAT);
 
-  case VALIDITY_UNKNOWN:
-    return Result(SAT_UNKNOWN, d_unknownExplanation);
+    case VALIDITY_UNKNOWN:
+      return Result(SAT_UNKNOWN, d_unknownExplanation);
 
-  default:
-    Unhandled(d_validity);
+    default:
+      Unhandled(d_validity);
+    }
   }
+
+  // TYPE_NONE
+  return Result(SAT_UNKNOWN, NO_STATUS);
 }
 
-Result Result::asValidityResult() const {
+Result Result::asValidityResult() const throw() {
   if(d_which == TYPE_VALIDITY) {
     return *this;
   }
 
-  Assert(d_which == TYPE_SAT);
-
-  switch(d_sat) {
+  if(d_which == TYPE_SAT) {
+    switch(d_sat) {
 
-  case SAT:
-    return Result(INVALID);
+    case SAT:
+      return Result(INVALID);
 
-  case UNSAT:
-    return Result(VALID);
+    case UNSAT:
+      return Result(VALID);
 
-  case SAT_UNKNOWN:
-    return Result(VALIDITY_UNKNOWN, d_unknownExplanation);
+    case SAT_UNKNOWN:
+      return Result(VALIDITY_UNKNOWN, d_unknownExplanation);
 
-  default:
-    Unhandled(d_sat);
+    default:
+      Unhandled(d_sat);
+    }
   }
+
+  // TYPE_NONE
+  return Result(VALIDITY_UNKNOWN, NO_STATUS);
 }
 
 string Result::toString() const {
@@ -164,6 +170,7 @@ ostream& operator<<(ostream& out,
   case Result::INCOMPLETE: out << "INCOMPLETE"; break;
   case Result::TIMEOUT: out << "TIMEOUT"; break;
   case Result::MEMOUT: out << "MEMOUT"; break;
+  case Result::NO_STATUS: out << "NO_STATUS"; break;
   case Result::OTHER: out << "OTHER"; break;
   case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
   default: Unhandled(e);

diff --git a/src/util/result.h b/src/util/result.h
index 62ddc74d00a47bed14ea152e098a782850442ede..1e07293321b59f94506d6a9e5946d969e467c253 100644 (file)
--- 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);
 }
 

diff --git a/test/Makefile b/test/Makefile
index 45659ae1ea6f9e16529005c5d876a2a4c7c35dfb..d1ebf4bb9d71cf9b17d79ac5ceb3438e5665473b 100644 (file)
--- a/test/Makefile
+++ b/test/Makefile
@@ -4,5 +4,5 @@ srcdir = test
 include $(topdir)/Makefile.subdir
 
 # synonyms for "check"
-.PHONY: regress test
-regress test: check
+.PHONY: test
+test: check

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 9bc8991ab2450e9adb63e0f57f5a7ce7334589cf..019eda76d8e78909415bf29026a934d957211d29 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -82,7 +82,8 @@ BUG_TESTS = \
        bug164.smt \
        bug167.smt \
        bug168.smt \
-       bug187.smt2
+       bug187.smt2 \
+       bug220.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/bug220.smt2 b/test/regress/regress0/bug220.smt2
new file mode 100644 (file)
index 0000000..117ee3b
--- /dev/null
+++ b/test/regress/regress0/bug220.smt2
@@ -0,0 +1,2 @@
+% EXIT: 0
+(exit)

diff --git a/test/regress/regress0/uf/bug217.smt2 b/test/regress/regress0/uf/bug217.smt2
new file mode 100644 (file)
index 0000000..45f0f3c
--- /dev/null
+++ b/test/regress/regress0/uf/bug217.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-fun f (Bool) Bool)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+;(assert (and x (or (f x) (f y))))
+(assert (or (f x) (f y) (f z)))
+(assert (not (f false)))
+(assert (not (f true)))
+(check-sat)
+;(get-value ((f true) (f false) (f x) (f y) (f z) x y z))

diff --git a/test/system/Makefile b/test/system/Makefile
index 2ca4091cb0c79b4253ab1ba3b9a5a637787ce7c8..87b92bb11d78c8250c0f0463c309a19f8cddd26f 100644 (file)
--- a/test/system/Makefile
+++ b/test/system/Makefile
@@ -4,5 +4,5 @@ srcdir = test/system
 include $(topdir)/Makefile.subdir
 
 # synonyms for "check"
-.PHONY: regress test
-regress test: check
+.PHONY: test
+test: check

diff --git a/test/unit/Makefile b/test/unit/Makefile
index 94a9d1d9e320fa22ed3228afd9f0533f404c241c..16dc971e11765c6cb988c62822400cc2720e26ac 100644 (file)
--- a/test/unit/Makefile
+++ b/test/unit/Makefile
@@ -4,5 +4,5 @@ srcdir = test/unit
 include $(topdir)/Makefile.subdir
 
 # synonyms for "check"
-.PHONY: regress test
-regress test: check
+.PHONY: test
+test: check