From 4f33c123c99b8a6d0ef519db001e62b626abe112 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Feb 2020 20:31:05 -0800 Subject: [PATCH] add placeholder Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 8f81d2096..c1d941064 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1136,7 +1136,11 @@ public: TRACE("arith", tout << "sort constraint: " << mk_pp(n->get_owner(), m) << "\n";); if (!th.is_attached_to_var(n)) { theory_var v = mk_var(n->get_owner(), false); - register_theory_var_in_lar_solver(v); + auto vi = register_theory_var_in_lar_solver(v); + expr* e = nullptr; + if (a.is_to_real(n->get_owner(), e)) { + // TBD: add a way to bind equality between vi and wi in m_solver + } } }