mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

adding benign initialization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-08 10:50:06 -07:00
parent 579b914d78
commit d8c3b273d3
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -10059,7 +10059,7 @@ namespace smt {
}
TRACE("str", tout << "last bounds are [" << lastBounds.lowerBound << " | " << lastBounds.midPoint << " | " << lastBounds.upperBound << "]!" << lastBounds.windowSize << std::endl;);
binary_search_info newBounds;
expr * newTester;
expr * newTester = 0;
if (lastTesterConstant == "more") {
// special case: if the midpoint, upper bound, and window size are all equal,
// we double the window size and adjust the bounds