diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index cecfb95cc..04b73ebc9 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -553,6 +553,7 @@ namespace polysat { clause_ref slicing::conflict_clause() { NOT_IMPLEMENTED_YET(); // TODO: call explain and build clause as described in notes at the top + return {}; } void slicing::egraph_on_propagate(enode* lit, enode* ante) {