summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/unit/theory/regexp_operation_black.h7
1 files changed, 6 insertions, 1 deletions
diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h
index 6e01392ab..551d59bef 100644
--- a/test/unit/theory/regexp_operation_black.h
+++ b/test/unit/theory/regexp_operation_black.h
@@ -25,7 +25,9 @@
#include "expr/node_manager.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
+#include "theory/rewriter.h"
#include "theory/strings/regexp_operation.h"
+#include "theory/strings/skolem_cache.h"
using namespace CVC4;
using namespace CVC4::kind;
@@ -46,7 +48,8 @@ class RegexpOperationBlack : public CxxTest::TestSuite
d_em = d_slv->getExprManager();
d_smt = d_slv->getSmtEngine();
d_scope = new SmtScope(d_smt);
- d_regExpOpr = new RegExpOpr();
+ d_skc = new SkolemCache();
+ d_regExpOpr = new RegExpOpr(d_skc);
// Ensure that the SMT engine is fully initialized (required for the
// rewriter)
@@ -58,6 +61,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite
void tearDown() override
{
delete d_regExpOpr;
+ delete d_skc;
delete d_scope;
delete d_slv;
}
@@ -153,6 +157,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite
ExprManager* d_em;
SmtEngine* d_smt;
SmtScope* d_scope;
+ SkolemCache* d_skc;
RegExpOpr* d_regExpOpr;
NodeManager* d_nm;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback