Linux Driver Verification » BLAST

For example, on my machine, limiting -resource helps. Here's the output:

$ src/bin/cvc3 -lang smtlib <smt_query_short -resource 5
unsat
$ src/bin/cvc3 -lang smtlib <smt_query_long  -resource 5
unknown

An option -quant-complete-inst may be used. It disables complete instantiation heuristic, i.e. instantiating every forall quantified subexpression with all possible terms. This significantly decreases the number of resulting instances and thus time and memory consumption (with this option cvc3 gives "unknown" on smt_query_long example in ~15 seconds). Also an option -quant-max-IL n (where n is maximal instantiation level allowed) may help. It puts a limit on the number of repeated instantiations with ground terms that have appeared as a result of some previous instantiations. The "depth" of such repeated instantiation is called instantiation level. There is a soft time limit option -stimeout ms (in tenth of seconds). "Currently, when the limit is reached, cvc3 tries to quickly terminate, probably with the status unknown", cvc3 documentation says.

On small regression tests cvc3 performed worse with only -quant-complete-inst option. It consumed much more time and memory and even got out of 2GB limit on some tests. Maybe some other instantiation heuristic was used... So I added -quant-new option disabling all instantiation heuristics except naive. Then test results restored.

Should we give -quant-new option more usable name and push it to upstream?

Alexey Khoroshilov wrote:

Should we give -quant-new option more usable name and push it to upstream?

This is and option from upstream. Michael was talking about "adding" it to the list of options to launch experiments on, not about "adding it to the tool". :-)

(somehow the comment haven't got posted...)

Should this issue be closed?