Fix type checking for define-funs (resolves bug 398).

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 2 insertions, 2 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cedd866f9..ad72e0737 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -888,7 +888,7 @@ void SmtEngine::defineFunction(Expr func,
   // doesn't match the SMT-LIBv2 standard...
   if(formals.size() > 0) {
     Type rangeType = FunctionType(funcType).getRangeType();
-    if(formulaType != rangeType) {
+    if(! formulaType.isComparableTo(rangeType)) {
       stringstream ss;
       ss << "Type of defined function does not match its declaration\n"
          << "The function  : " << func << "\n"
@@ -898,7 +898,7 @@ void SmtEngine::defineFunction(Expr func,
       throw TypeCheckingException(func, ss.str());
     }
   } else {
-    if(formulaType != funcType) {
+    if(! formulaType.isComparableTo(funcType)) {
       stringstream ss;
       ss << "Declared type of defined constant does not match its definition\n"
          << "The constant   : " << func << "\n"