projects
/
cvc5.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
Preparation for models for co-inductive datatypes. Minor cleanup.
[cvc5.git]
/
src
/
theory
/
quantifiers_engine.cpp
diff --git
a/src/theory/quantifiers_engine.cpp
b/src/theory/quantifiers_engine.cpp
index 1837a34f45f8f32707d6bebe41c4c444685263a9..be011cdb6b340f1090e096aea1d0b51e2381942b 100644
(file)
--- a/
src/theory/quantifiers_engine.cpp
+++ b/
src/theory/quantifiers_engine.cpp
@@
-109,12
+109,6
@@
d_lemmas_produced_c(u){
}
//options
- d_optInstCheckDuplicate = true;
- d_optInstMakeRepresentative = true;
- d_optInstAddSplits = false;
- d_optMatchIgnoreModelBasis = false;
- d_optInstLimitActive = false;
- d_optInstLimit = 0;
d_total_inst_count_debug = 0;
}