mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

clean up a trace statement

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-03 21:18:51 -08:00
parent 20af3dd675
commit 11995e58f4
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_lra.cpp
View file

@ -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));

5
src/test/lp/CMakeLists.txt
View file

@ -1,6 +1,9 @@
add_executable(lp_tst
EXCLUDE_FROM_ALL
lp_main.cpp lp.cpp nla_solver_test.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:polynomial> $<TARGET_OBJECTS:nlsat> $<TARGET_OBJECTS:lp> )
lp_main.cpp lp.cpp nla_solver_test.cpp $<TARGET_OBJECTS:util>
$<TARGET_OBJECTS:polynomial> $<TARGET_OBJECTS:nlsat>
$<TARGET_OBJECTS:lp> $<TARGET_OBJECTS:grobner>
$<TARGET_OBJECTS:interval> $<TARGET_OBJECTS:dd> $<TARGET_OBJECTS:ast>)
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})