mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-25 23:40:05 -07:00
parent 848bfb14a1
commit ba1630f380
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/sls_solver.h
View file

@ -52,8 +52,6 @@ namespace sls {
#else
#include <thread>
#include <mutex>
#include "ast/sls/sls_smt_plugin.h"
namespace euf {

4
src/test/dlist.cpp
View file

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

2
src/test/sls_test.cpp
View file

@ -16,7 +16,7 @@ namespace bv {
vector<sat::clause_info> const& clauses() const override { return m_clauses; }
sat::clause_info const& get_clause(unsigned idx) const override { return m_clauses[idx]; }
ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return ptr_iterator<unsigned>(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; }