diff options
Diffstat (limited to 'src/theory/strings/theory_strings_preprocess.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a752958b2..084e2ac91 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -19,6 +19,7 @@ #include <stdint.h> #include "expr/kind.h" +#include "options/smt_options.h" #include "options/strings_options.h" #include "proof/proof_manager.h" #include "smt/logic_exception.h" @@ -972,7 +973,10 @@ void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){ : NodeManager::currentNM()->mkNode(kind::AND, asserts); if( res!=vec_node[i] ){ res = Rewriter::rewrite( res ); - PROOF( ProofManager::currentPM()->addDependence( res, vec_node[i] ); ); + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(res, vec_node[i]); + } vec_node[i] = res; } } |