Fix argument in nonlinear extension. (#3216)

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 1f6e1388a7a9a8ce47194647ebdb96dbcc8086df..f067fda4758196a99919353a8d0c538edb3da6d8 100644 (file)
--- 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);