FP: Remove static call to Rewriter. (#7765)

diff --git a/src/theory/fp/fp_word_blaster.h b/src/theory/fp/fp_word_blaster.h
index f9ec4fd4eac010f8b0038ed270dc96a0e3a892d2..f7c7f26beea700eb45917cb7683c7d4552421648 100644 (file)
--- a/src/theory/fp/fp_word_blaster.h
+++ b/src/theory/fp/fp_word_blaster.h
@@ -34,15 +34,6 @@
 #include "util/floatingpoint_size.h"
 #include "util/hash.h"
 
-#ifdef CVC5_SYM_SYMBOLIC_EVAL
-// This allows debugging of the cvc5 symbolic back-end.
-// By enabling this and disabling constant folding in the rewriter,
-// SMT files that have operations on constants will be evaluated
-// during the encoding step, which means that the expressions
-// generated by the symbolic back-end can be debugged with gdb.
-#include "theory/rewriter.h"
-#endif
-
 namespace cvc5 {
 namespace theory {
 namespace fp {
@@ -100,16 +91,7 @@ typedef traits::bwt bwt;
 class nodeWrapper : public Node
 {
  protected:
-/* CVC5_SYM_SYMBOLIC_EVAL is for debugging cvc5 symbolic back-end issues.
- * Enable this and disabling constant folding will mean that operations
- * that are input with constant args are 'folded' using the symbolic encoding
- * allowing them to be traced via GDB.
- */
-#ifdef CVC5_SYM_SYMBOLIC_EVAL
-  nodeWrapper(const Node& n) : Node(theory::Rewriter::rewrite(n)) {}
-#else
   nodeWrapper(const Node& n) : Node(n) {}
-#endif
 };
 
 class symbolicProposition : public nodeWrapper