From 025e4b90cab09c4d4a9b83ede1b0ed9d8d03299d Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Mon, 5 Nov 2018 22:30:08 -0800
Subject: [PATCH] add a constant to the context trail

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index a3249e5da..30ded0549 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -411,6 +411,7 @@ class theory_lra::imp {
         TRACE("arith", tout << "add " << cnst << "\n";);
         mk_enode(cnst);
         theory_var v = mk_var(cnst);
+        ctx().push_trail(value_trail<smt::context, lp::var_index>(var));
         var = m_solver->add_var(v, true);
         m_theory_var2var_index.setx(v, var, UINT_MAX);
         m_var_index2theory_var.setx(var, v, UINT_MAX);