diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h index d14b403c9..35f4e1b7d 100644 --- a/src/sat/smt/sls_solver.h +++ b/src/sat/smt/sls_solver.h @@ -52,8 +52,6 @@ namespace sls { #else -#include -#include #include "ast/sls/sls_smt_plugin.h" namespace euf { diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index 9ad04d6b2..e378ddec7 100644 --- a/src/test/dlist.cpp +++ b/src/test/dlist.cpp @@ -106,6 +106,7 @@ static void test_insert_before() { std::cout << "test_insert_before passed." << std::endl; } +#if 0 // Test the remove_from() method static void test_remove_from() { TestNode* list = nullptr; @@ -119,6 +120,7 @@ static void test_remove_from() { SASSERT(node2.prev() == &node2); std::cout << "test_remove_from passed." << std::endl; } +#endif // Test the push_to_front() method static void test_push_to_front() { @@ -179,6 +181,6 @@ void tst_dlist() { test_detach(); test_invariant(); test_contains(); - (void)test_remove_from; + //test_remove_from; std::cout << "All tests passed." << std::endl; } diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp index b40261df3..fe96a5dd9 100644 --- a/src/test/sls_test.cpp +++ b/src/test/sls_test.cpp @@ -16,7 +16,7 @@ namespace bv { vector const& clauses() const override { return m_clauses; } sat::clause_info const& get_clause(unsigned idx) const override { return m_clauses[idx]; } ptr_iterator get_use_list(sat::literal lit) override { return ptr_iterator(nullptr, nullptr); } - bool flip(sat::bool_var v) override { return true; } + void flip(sat::bool_var v) override { } double reward(sat::bool_var v) override { return 0; } double get_weigth(unsigned clause_idx) override { return 0; } bool is_true(sat::literal lit) override { return true; }