We observe such a mismatch in tests that contain expressions of the form
(bvadd t_1 ... t_n) , or(bvmul t_1 ... t_n)
The test cannot explicitly indicate this term. For example, the term (bvadd a (bvsub b (bvadd cd)) simplified to the nary sum.
In many cases, the order of the terms t_i has a significant impact on performance. Variable names affect the order of these conditions. Z3 has two simplifications of the formula.
The old one (located in src/ast/simplifier ) uses the internal identifiers associated with each expression to sort the arguments of the AC operators. This approach is not affected by name changes, but it has another unpleasant side effect: the order of expressions we created affects the internal assignment of the identifier and, therefore, the order of the terms t_i . This has been a problem in many Z3 applications.
The new simplifier (located in src/ast/rewriter ) takes a different approach. It sorts expressions using a general order based on the structure of expressions. In this new approach, the order we create does not matter, but the names do. New code uses this new formula simplifier. However, we still have the old code that uses the old simplifier.
The QF_AUFBV tests use both simplifications of the formula. This will change in the future, after we replace all occurrences of the old simplifier with a new one.
Finally, it would be great if you could send us a set of tests in which you have performance problems. This will help us improve the Z3.
EDIT
I would like to emphasize that the main problem is the appearance of form expressions (bvadd t_1 ... t_n) . Secondly, both simplifications are used for QF_AUFBV tests. In the current version, it is difficult to avoid these time fluctuations. For example, we should also observe temporal fluctuations if we reorder assumptions.
Here is a description of what happens in your instance, and why the name affects the behavior. This is a bit technical, but he needs to clarify what is happening.
1- The new simplifier is completed. This simplifier caches intermediate results using a hash table. The AST hash code depends on the names used for constants and function characters.
2- After completing the new simplification, the cache will be deleted. We go through the AST stored in the cache and decrease their control counters. If the counter is zero, the AST is deleted. IMPORTANT: the order of the AST in the hash table depends on their hash code. Thus, the hash code (and therefore the names) can affect the order AST removes.
3. The AST manager in Z3 assigns an internal identifier to each AST node. When the AST node is deleted, its identifier is processed. That is, an identifier can be assigned to new AST nodes. We do this because we do not want to end identifiers.
4- When the old simplifier is completed, it will create new ASTs, and the processed identifiers will be assigned to these new ASTs.
5- Since the old simplifier uses identifiers to sort bvadd arguments, we can get a different order when we change the variable name.
Summary
Different name ==> Miscellaneous Hash ==> Different order in the Hashtable ==> Different delete orders ==> Secondary identifiers are reused in a different order ==> new ASTs with different identifiers ==> Affects how the old simplifier orders the arguments bvadd