diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-02 16:51:03 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-02 16:51:03 -0700 |
| commit | be08eae24750b006d8a4b1e27e0e242553f64735 (patch) | |
| tree | f467d044a1166055fd10d91f2d21239c215ff869 /test/unit | |
| parent | afd4d46b2559c9bb3427678ca287c33d3923ef7f (diff) | |
Refactor ApplySubsts preprocessing pass. (#2120)
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/preprocessing/pass_bv_gauss_white.h | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index cdf620285..7d7ee1a3a 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -14,14 +14,15 @@ ** Unit tests for Gaussian Elimination preprocessing pass. **/ +#include "context/context.h" #include "expr/node.h" #include "expr/node_manager.h" -#include "preprocessing/preprocessing_pass.h" #include "preprocessing/passes/bv_gauss.cpp" +#include "preprocessing/preprocessing_pass.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "theory/rewriter.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" #include "util/bitvector.h" #include <cxxtest/TestSuite.h> @@ -2377,7 +2378,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - AssertionPipeline apipe; + context::Context context; + AssertionPipeline apipe(&context); apipe.push_back(a); passes::BVGauss bgauss(nullptr); std::unordered_map<Node, Node, NodeHashFunction> res; @@ -2459,7 +2461,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - AssertionPipeline apipe; + context::Context context; + AssertionPipeline apipe(&context); apipe.push_back(a); apipe.push_back(eq4); apipe.push_back(eq5); @@ -2510,7 +2513,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_p), d_nine); - AssertionPipeline apipe; + context::Context context; + AssertionPipeline apipe(&context); apipe.push_back(eq1); apipe.push_back(eq2); passes::BVGauss bgauss(nullptr); |