From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 15 Nov 2019 13:59:38 +0000 (-0600)
Subject: Fix wrong kind in sygus version 1 parser (#3463)
X-Git-Tag: cvc5-1.0.0~3838
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d43fe797c2ec03b76dd55cdb5485fb62d0dfb3a;p=cvc5.git

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

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8031e81e6..ae0607b53 100644
--- 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 0d953c19e..0312c13b7 100644
--- 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
index 000000000..1f839c229
--- /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)