From 2b673bcb486d55857c21e7d80a47eb34476bd746 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 12:56:00 -0800 Subject: [PATCH] remove component dependency on bigfix Signed-off-by: Nikolaj Bjorner --- src/math/polysat/CMakeLists.txt | 1 - src/math/polysat/clause.h | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index cf0e36479..2986cb94e 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -32,7 +32,6 @@ z3_add_component(polysat viable.cpp viable_fallback.cpp COMPONENT_DEPENDENCIES - bigfix dd euf interval diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h index c1c3170bb..b951be24d 100644 --- a/src/math/polysat/clause.h +++ b/src/math/polysat/clause.h @@ -24,7 +24,7 @@ namespace polysat { // NB code review: // right, ref-count is unlikely the right mechanism. // In the SAT solver all clauses are managed in one arena (auxiliarary and redundant) - // and deleted when they exist the arena. + // and deleted when they exit the arena. // class clause { public: