From b8f076a07213b8e3be83a9b9a086418ce5aab94f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Mar 2020 12:59:14 -0800
Subject: [PATCH] fix #3121

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index c0fb96a8b..6617e2211 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3087,6 +3087,28 @@ public:
 
     bool set_lower_bound(lpvar vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, true);   }
 
+    vector<constraint_bound> m_history;
+    template<typename Ctx, typename T, bool CallDestructors=true>
+    class history_trail : public trail<Ctx> {
+        vector<T, CallDestructors> & m_dst;
+        unsigned                     m_idx;
+        vector<T, CallDestructors> & m_hist;
+    public:
+        history_trail(vector<T, CallDestructors> & v, unsigned idx, vector<T, CallDestructors> & hist):
+            m_dst(v),
+            m_idx(idx),
+            m_hist(hist) {}
+
+        ~history_trail() override {
+        }
+
+        void undo(Ctx & ctx) override {
+            m_dst[m_idx] = m_hist.back();
+            m_hist.pop_back();
+        }
+    };
+
+
     bool set_bound(lpvar vi, lp::constraint_index ci, rational const& v, bool is_lower) {
 
         if (lp().is_term(vi)) {
@@ -3098,7 +3120,8 @@ public:
             constraint_bound& b = vec[ti];
             if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) {
                 TRACE("arith", tout << "tighter bound " << vi << "\n";);
-                ctx().push_trail(vector_value_trail<context, constraint_bound>(vec, ti));
+                m_history.push_back(vec[ti]);
+                ctx().push_trail(history_trail<context, constraint_bound>(vec, ti, m_history));
                 b.first = ci;
                 b.second = v;
             }