diff options
Diffstat (limited to 'test/unit/theory/theory_arith_cad_white.cpp')
| -rw-r--r-- | test/unit/theory/theory_arith_cad_white.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp index 4c9b104c7..3d5f7a8c5 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -29,7 +29,7 @@ #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/poly_conversion.h" #include "theory/arith/theory_arith.h" -#include "theory/quantifiers/extended_rewrite.h" +#include "theory/rewriter.h" #include "theory/theory.h" #include "theory/theory_engine.h" #include "util/poly_util.h" @@ -193,8 +193,7 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_simp) EXPECT_NE(rewritten, d_nodeManager->mkConst(false)); } { - quantifiers::ExtendedRewriter extrew; - Node rewritten = extrew.extendedRewrite(orig); + Node rewritten = Rewriter::callExtendedRewrite(orig); EXPECT_EQ(rewritten, d_nodeManager->mkConst(false)); } } |