diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-11 15:36:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-11 13:36:38 -0700 |
commit | 1339e2a3b884d34a9c27eb45bb6847a493fe0365 (patch) | |
tree | eee01493ebe789c8c1b09e5f977273c360a52bc7 /src/theory/quantifiers/instantiate.h | |
parent | 1c859fd0f43fa2081bdb247423e81d9174a5f474 (diff) |
Remove instantiation model true option (#4861)
This was an option that rejected instantiations that are true according to the current
model's equality engine.
This option was never helpful and will be burdensome to maintain with new updates
to equality engine infrastructure.
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 16ff1f2c3..cb40bbbbc 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -305,7 +305,6 @@ class Instantiate : public QuantifiersUtil IntStat d_inst_duplicate; IntStat d_inst_duplicate_eq; IntStat d_inst_duplicate_ent; - IntStat d_inst_duplicate_model_true; Statistics(); ~Statistics(); }; /* class Instantiate::Statistics */ |