Fix wrong kind in sygus version 1 parser (#3463)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8031e81e6259e56b3774861966566e17ed193e2e..ae0607b538ca6807cd7f2f7d3f4bc86e9807f3e0 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1302,7 +1302,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         }
         children.insert(children.end(), largs.begin(), largs.end());
         Kind sk = ops[i].getKind() != kind::BUILTIN
-                      ? kind::APPLY_UF
+                      ? getKindForFunction(ops[i])
                       : getExprManager()->operatorToKind(ops[i]);
         Expr body = getExprManager()->mkExpr(sk, children);
         // replace by lambda

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0d953c19e52eaf84aed927276924ac8c1763cbf9..0312c13b7ab77256542ecdd31e80d8bd1f515f7f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1717,6 +1717,7 @@ set(regress_1_tests
   regress1/sygus/issue3205.smt2
   regress1/sygus/issue3247.smt2
   regress1/sygus/issue3320-quant.sy
+  regress1/sygus/issue3461.sy
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy

diff --git a/test/regress/regress1/sygus/issue3461.sy b/test/regress/regress1/sygus/issue3461.sy
new file mode 100644 (file)
index 0000000..1f839c2
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3461.sy
@@ -0,0 +1,17 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic ALL_SUPPORTED)
+
+(declare-datatype Doc ((D (owner Int) (body Int))))
+
+(declare-datatype Policy 
+  ((p (principal Int)) 
+   (por (left Policy) (right Policy))))
+
+(synth-fun mkPolicy ((d Doc)) Policy
+  ((Start Policy (Q))
+   (Q Policy ((p 0) (p 1) (por Q Q))))
+)
+
+(check-synth)