summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp7
1 files changed, 3 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f203c7d1e..a4f18e57b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3297,10 +3297,9 @@ void SmtEnginePrivate::processAssertions() {
if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
dumpAssertions("pre-strings-pp", d_assertions);
- ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() );
- //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
- //}
+ if( !options::stringLazyPreproc() ){
+ ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() );
+ }
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
dumpAssertions("post-strings-pp", d_assertions);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback