diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-08 15:32:38 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-08 13:32:38 -0700 |
commit | 16b54708ff83a1bf6393203b79da6dc059fd2025 (patch) | |
tree | d4f7100dc4e1ea90c881c5dba13ae102d73afba9 /src | |
parent | e7929d2cd241d8b4974d26b9e11f1378ba30b0e7 (diff) |
Fix method for getting arithmetic function definition body (#3371)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 87d6ec0c3..f5ebb33b1 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -157,14 +157,14 @@ Node QuantAttributes::getFunDefBody( Node q ) { { // solve for h in the equality std::map<Node, Node> msum; - if (ArithMSum::getMonomialSum(q[1], msum)) + if (ArithMSum::getMonomialSumLit(q[1], msum)) { Node veq; int res = ArithMSum::isolate(h, msum, veq, EQUAL); if (res != 0) { Assert(veq.getKind() == EQUAL); - return res == 1 ? veq[0] : veq[1]; + return res == 1 ? veq[1] : veq[0]; } } } |