diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 13:35:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-14 13:35:53 -0600 |
| commit | e16ab44a2b4622bb5745633cbafd43a0023a518c (patch) | |
| tree | d980bdc3dc771abfc8101036d1e2aaebc8020134 /src/theory/sets/theory_sets_rewriter.cpp | |
| parent | ad34df900d79aad64558b354a866870715bfd007 (diff) | |
| parent | effb0d47ba5bfaebae17dcd06153489dccd90eff (diff) | |
Merge branch 'master' into cav22-stringscav22-strings
Diffstat (limited to 'src/theory/sets/theory_sets_rewriter.cpp')
| -rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index d603946c4..cb9b26731 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -272,13 +272,12 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { { if(node[0].isConst()) { std::set<Node> elements = NormalForm::getElementsFromNormalConstant(node[0]); - return RewriteResponse( - REWRITE_DONE, nm->mkConst(CONST_RATIONAL, Rational(elements.size()))); + return RewriteResponse(REWRITE_DONE, + nm->mkConstInt(Rational(elements.size()))); } else if (node[0].getKind() == kind::SET_SINGLETON) { - return RewriteResponse(REWRITE_DONE, - nm->mkConst(CONST_RATIONAL, Rational(1))); + return RewriteResponse(REWRITE_DONE, nm->mkConstInt(Rational(1))); } else if (node[0].getKind() == kind::SET_UNION) { |