mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

tabs to spaces test

Browse source
This commit is contained in:
Murphy Berzish 2016-11-17 15:28:17 -05:00
parent e2d05578d6
commit d260218e2b
1 changed files with 17 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/smt/theory_str.cpp
View file

@ -35,13 +35,13 @@ theory_str::theory_str(ast_manager & m):
opt_AggressiveUnrollTesting(true),
opt_EagerStringConstantLengthAssertions(true),
opt_VerifyFinalCheckProgress(true),
opt_LCMUnrollStep(2),
opt_NoQuickReturn_IntegerTheory(false),
opt_DisableIntegerTheoryIntegration(false),
opt_DeferEQCConsistencyCheck(false),
opt_CheckVariableScope(true),
opt_UseFastLengthTesterCache(true),
opt_UseFastValueTesterCache(true),
opt_LCMUnrollStep(2),
opt_NoQuickReturn_IntegerTheory(false),
opt_DisableIntegerTheoryIntegration(false),
opt_DeferEQCConsistencyCheck(false),
opt_CheckVariableScope(true),
opt_UseFastLengthTesterCache(true),
opt_UseFastValueTesterCache(true),
/* Internal setup */
search_started(false),
m_autil(m),
@ -51,17 +51,17 @@ theory_str::theory_str(ast_manager & m):
m_trail(m),
m_delayed_axiom_setup_terms(m),
tmpStringVarCount(0),
tmpXorVarCount(0),
tmpLenTestVarCount(0),
tmpValTestVarCount(0),
avoidLoopCut(true),
loopDetected(false),
contains_map(m),
string_int_conversion_terms(m),
m_find(*this),
m_trail_stack(*this)
tmpXorVarCount(0),
tmpLenTestVarCount(0),
tmpValTestVarCount(0),
avoidLoopCut(true),
loopDetected(false),
contains_map(m),
string_int_conversion_terms(m),
m_find(*this),
m_trail_stack(*this)
{
initialize_charset();
initialize_charset();
}
theory_str::~theory_str() {