Fix ascription check for return types on ordinary functions (#7290)

Fixes #7274.

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 39b38be30563ea73dd22c8be923b6257a009ec6b..84c0bd17c632721ca7c486ada55cad04aa05c389 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -598,13 +598,19 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
     }
     return t;
   }
-  // otherwise, nothing to do
-  // check that the type is correct
-  if (t.getSort() != s)
+  // Otherwise, check that the type is correct. Type ascriptions in SMT-LIB 2.6
+  // referred to the range of function sorts. Note that this is only a check
+  // and does not impact the returned term.
+  api::Sort checkSort = t.getSort();
+  if (checkSort.isFunction())
+  {
+    checkSort = checkSort.getFunctionCodomainSort();
+  }
+  if (checkSort != s)
   {
     std::stringstream ss;
-    ss << "Type ascription not satisfied, term " << t << " expected sort " << s
-       << " but has sort " << t.getSort();
+    ss << "Type ascription not satisfied, term " << t
+       << " expected (codomain) sort " << s << " but has sort " << t.getSort();
     parseError(ss.str());
   }
   return t;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3bfe356fac63121e58d5fd1bececd35c0eabccfd..768fe852f66bac1deba0bc0b007bb0c879d47a06 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -779,6 +779,7 @@ set(regress_0_tests
   regress0/parser/force_logic_set_logic.smt2
   regress0/parser/force_logic_success.smt2
   regress0/parser/issue5163.smt2
+  regress0/parser/issue7274.smt2
   regress0/parser/linear_arithmetic_err1.smt2
   regress0/parser/linear_arithmetic_err2.smt2
   regress0/parser/linear_arithmetic_err3.smt2

diff --git a/test/regress/regress0/parser/issue7274.smt2 b/test/regress/regress0/parser/issue7274.smt2
new file mode 100644 (file)
index 0000000..c7a38d0
--- /dev/null
+++ b/test/regress/regress0/parser/issue7274.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun f (Int) Int)
+(declare-fun g1 (Int) Int)
+(declare-fun x () Int)
+(assert (= ((as f Int) x) (g1 x)))
+(check-sat)