diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f60de5c4f..6460af4b9 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -730,10 +730,10 @@ namespace smt { m_asserted_qhead(0), m_assume_eq_head(0), m_num_conflicts(0), + m_use_nra_model(false), m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)), m_solver(0), - m_resource_limit(*this), - m_use_nra_model(false) { + m_resource_limit(*this) { } ~imp() { diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 0f9fa938a..0b5508ec9 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1,7 +1,7 @@ #include "util/lp/lar_solver.h" /* Copyright (c) 2017 Microsoft Corporation - Author: Lev Nachmanson + Author: Nikolaj Bjorner, Lev Nachmanson */ namespace lp { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 668968122..7f700bd75 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -10,7 +10,7 @@ Abstract: Author: - + Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) Revision History: diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp index efa003b37..327d2b70f 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/util/lp/nra_solver.cpp @@ -1,6 +1,6 @@ /* Copyright (c) 2017 Microsoft Corporation - Author: Lev Nachmanson + Author: Nikolaj Bjorner */ #include "util/lp/lar_solver.h" diff --git a/src/util/lp/nra_solver.h b/src/util/lp/nra_solver.h index 68c9e98e5..70e614e91 100644 --- a/src/util/lp/nra_solver.h +++ b/src/util/lp/nra_solver.h @@ -1,6 +1,6 @@ /* Copyright (c) 2017 Microsoft Corporation - Author: Lev Nachmanson + Author: Nikolaj Bjorner */ #pragma once