diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-29 18:24:43 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-29 18:24:43 -0600 |
| commit | 47d542f312ac8e22e8d3aae1007cfd13701983a6 (patch) | |
| tree | 5d1f0062fa535f5f64528ff3e2b110e7456f2f52 /src/options/quantifiers_options | |
| parent | 0b821fa27929b5a65ce78767d26a21f779a82d3d (diff) | |
Cbqi repeat solve literal (#1458)
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 65731547d..27671fd82 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -311,6 +311,8 @@ option cbqiAll --cbqi-all bool :read-write :default false apply counterexample-based instantiation to all quantified formulas option cbqiMultiInst --cbqi-multi-inst bool :read-write :default false when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation +option cbqiRepeatLit --cbqi-repeat-lit bool :read-write :default false + solve literals more than once in counterexample-based quantifier instantiation # CEGQI for arithmetic option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false |