diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-23 12:29:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-23 12:29:58 -0500 |
| commit | 5f384849d20c915374c7b189a232c5d811c186ef (patch) | |
| tree | 26c830da54c5536cd28462ce4fd274e394b32314 /src/parser | |
| parent | 2a96d7de381aa565a6eacf724848c0e7839c7cf6 (diff) | |
Fix sygus datatype parsing in sygus v1 format (#3113)
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index af374274b..278f2bdfd 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1088,7 +1088,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st } } Kind sk = sop.getKind() != kind::BUILTIN - ? kind::APPLY_UF + ? getKindForFunction(sop) : getExprManager()->operatorToKind(sop); Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl; Expr e = getExprManager()->mkExpr( sk, children ); |