diff options
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3461.sy | 17 |
3 files changed, 19 insertions, 1 deletions
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) |