The current default time limit of 1 second already produces way too large constraints that cause a stack overflow in the recursive parser of Z3. Need to figure out how to deal with these.
The other limit currently implemented is a trace length limit (100 per default) that is not sufficient to represent the entire path in the tree for many of the array problems (which loop 10k times). However, perhaps we do not need to represent the full paths, just prefixes up to a certain length, so we can just stick with the trace length limit. Note: partial traces work fine in the current implementation.
The current default time limit of 1 second already produces way too large constraints that cause a stack overflow in the recursive parser of Z3. Need to figure out how to deal with these.
The other limit currently implemented is a trace length limit (100 per default) that is not sufficient to represent the entire path in the tree for many of the array problems (which loop 10k times). However, perhaps we do not need to represent the full paths, just prefixes up to a certain length, so we can just stick with the trace length limit. Note: partial traces work fine in the current implementation.