diff --git a/Makefile.build b/Makefile.build index 08c3629db..f1b700e9c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -87,7 +87,7 @@ MKVERSION=./utils/make_source_version srcdir = src srcsubdirs = mt io terms utils solvers solvers/floyd_warshall \ solvers/funs solvers/bv solvers/egraph solvers/cdcl solvers/simplex solvers/quant \ - parser_utils model scratch api frontend frontend/common \ + parser_utils model api frontend frontend/common \ frontend/smt1 frontend/yices frontend/smt2 context exists_forall \ mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/bv \ mcsat/bv/explain mcsat/utils diff --git a/src/Makefile b/src/Makefile index 9a14fc6ba..df9c0b000 100644 --- a/src/Makefile +++ b/src/Makefile @@ -436,9 +436,6 @@ extra_src_c := \ model/large_bvsets.c \ model/rb_bvsets.c \ model/small_bvsets.c \ - scratch/booleq_table.c \ - scratch/bool_vartable.c \ - scratch/update_graph.c \ solvers/bv/bvsolver_printer.c \ solvers/cdcl/clause_pool.c \ solvers/cdcl/gates_printer.c \ diff --git a/src/solvers/cdcl/smt_core.c b/src/solvers/cdcl/smt_core.c index efdd1a248..87cf21557 100644 --- a/src/solvers/cdcl/smt_core.c +++ b/src/solvers/cdcl/smt_core.c @@ -1588,7 +1588,8 @@ void init_smt_core(smt_core_t *s, uint32_t n, void *th, init_checkpoint_stack(&s->checkpoints); s->cp_flag = false; - s->etable = NULL; + // EXPERIMENTAL + // s->etable = NULL; s->trace = NULL; s->interrupt_push = false; diff --git a/src/solvers/cdcl/smt_core.h b/src/solvers/cdcl/smt_core.h index cc58d3b37..7d18a155b 100644 --- a/src/solvers/cdcl/smt_core.h +++ b/src/solvers/cdcl/smt_core.h @@ -63,7 +63,7 @@ // EXPERIMENTAL -#include "scratch/booleq_table.h" +// #include "scratch/booleq_table.h" /*********** @@ -1051,7 +1051,7 @@ typedef struct smt_core_s { bool cp_flag; // set true when backtracking. false when checkpoints are added /* EXPERIMENTAL (default to NULL) */ - booleq_table_t *etable; + // booleq_table_t *etable; /* Tracer object (default to NULL) */ tracer_t *trace; diff --git a/tests/unit/test_booleq_table.c b/tests/unit/test_booleq_table.c.disabled similarity index 100% rename from tests/unit/test_booleq_table.c rename to tests/unit/test_booleq_table.c.disabled