mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 01:02:15 +00:00
Code Activity

reorder initialization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-09 18:50:42 -07:00
parent d53e62a91c
commit 9b42068868
1 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/nlsat/nlsat_solver.cpp
View file

@ -1731,7 +1731,7 @@ namespace nlsat {
apply_reorder(); apply_reorder();
if (!m_incremental && m_inline_vars) { if (!m_incremental && m_inline_vars) {
if (!simplify()) if (!m_simplify())
return l_false; return l_false;
} }
IF_VERBOSE(3, verbose_stream() << "search\n"); IF_VERBOSE(3, verbose_stream() << "search\n");
@ -2791,9 +2791,6 @@ namespace nlsat {
*/ */
bool simplify() {
return m_simplify();
}
// Eliminated variables are tracked in m_bounds. // Eliminated variables are tracked in m_bounds.
// Each element in m_bounds tracks the eliminated variable and an upper or lower bound // Each element in m_bounds tracks the eliminated variable and an upper or lower bound