diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-03-22 13:37:11 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-03-22 13:37:11 +0000 |
| commit | 33239a85e160bcbdfa23b44e316065166e361af8 (patch) | |
| tree | 74d5c30a71e235edbe789dc63dc2e0378ef8f50d /src/expr/expr_manager_template.h | |
| parent | 74084011310e0af055c0055378620a5d19de1e52 (diff) | |
Merges the small changes on the queue-period branch into trunk. This branch importantly removes an unintentional line of code that had it pivoting more times than intended before rechecking the queue. Importantly, it does this without losing any examples with rewrite-equality enabled. This adds a parameter NUM_CHECKS which determines how many times the queue chould be checked during difference mode. A value of 10 for NUM_CHECKS has been empirically determined to be good in practice. See jobs 1815, 1824, 1825, 1821, 1814.
Diffstat (limited to 'src/expr/expr_manager_template.h')
0 files changed, 0 insertions, 0 deletions