diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-01 16:33:34 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-01 16:33:34 -0500 |
| commit | c3b5f9d57eaf17612170b7401465b75053b07985 (patch) | |
| tree | aeef3125d045a21bda899a7f2be22a1da50ebbc3 /src/expr | |
| parent | c365521b91520cf05739c7df6f2ae99f273c98d4 (diff) | |
Support sygus version 2 format (#3066)
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/datatype.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 3b925d0b1..5e1343bb0 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -180,7 +180,10 @@ void Datatype::addSygusConstructor(Expr op, { Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl; Debug("dt-sygus") << " sygus op : " << op << std::endl; - std::string name = getName() + "_" + cname; + // avoid name clashes + std::stringstream ss; + ss << getName() << "_" << getNumConstructors() << "_" << cname; + std::string name = ss.str(); std::string testerId("is-"); testerId.append(name); unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1); |