From ba1630f3805ee9eba1014dfc5602276b0179dc29 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Oct 2024 23:40:05 -0700 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/sat/smt/sls_solver.h | 2 -- src/test/dlist.cpp | 4 +++- src/test/sls_test.cpp | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) 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; }