From 11995e58f453abaf003d65a1313f00c98e89f876 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 3 Jan 2020 21:18:51 -0800 Subject: [PATCH] clean up a trace statement Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 5 ++++- src/test/lp/CMakeLists.txt | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 44daa7b43..24aba9266 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3127,7 +3127,10 @@ public: auto vi1 = register_theory_var_in_lar_solver(v1); auto vi2 = register_theory_var_in_lar_solver(v2); lp::constraint_index ci1, ci2, ci3, ci4; - TRACE("arith", tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << has_lower_bound(vi2, ci3, bound) << "\n";); + + TRACE("arith", + bool hlb = has_lower_bound(vi2, ci3, bound); + tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << hlb << std::endl;); if (has_lower_bound(vi2, ci3, bound) && has_upper_bound(vi2, ci4, bound)) { VERIFY (has_lower_bound(vi1, ci1, bound)); VERIFY (has_upper_bound(vi1, ci2, bound)); diff --git a/src/test/lp/CMakeLists.txt b/src/test/lp/CMakeLists.txt index e2873102d..76bb92e58 100644 --- a/src/test/lp/CMakeLists.txt +++ b/src/test/lp/CMakeLists.txt @@ -1,6 +1,9 @@ add_executable(lp_tst EXCLUDE_FROM_ALL -lp_main.cpp lp.cpp nla_solver_test.cpp $ $ $ $ ) +lp_main.cpp lp.cpp nla_solver_test.cpp $ +$ $ +$ $ +$ $ $) target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})