summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-08-23 10:44:29 -0500
committerGitHub <noreply@github.com>2019-08-23 10:44:29 -0500
commit996de9116150fb7214b3b9a56995e2492d3e5668 (patch)
treea663c243b67a514a1f015d91283a47353dde33b6 /src
parentfd385efcc6b1e55431430af4213172594781e05f (diff)
Fix argument in nonlinear extension. (#3216)
Diffstat (limited to 'src')
-rw-r--r--src/theory/arith/nonlinear_extension.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 1f6e1388a..f067fda47 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -2003,7 +2003,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
for (const Node& ac : a)
{
Node r =
- d_containing.getValuation().getModel()->getRepresentative(a[0]);
+ d_containing.getValuation().getModel()->getRepresentative(ac);
repList.push_back(r);
}
Node aa = argTrie[ak].add(a, repList);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback