From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Aug 2019 15:44:29 +0000 (-0500)
Subject: Fix argument in nonlinear extension. (#3216)
X-Git-Tag: cvc5-1.0.0~3999
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=996de9116150fb7214b3b9a56995e2492d3e5668;p=cvc5.git

Fix argument in nonlinear extension. (#3216)
---

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);