summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_split.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-09-13 13:36:28 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-09-13 13:36:28 -0500
commit5887766342258361d3635a5b29a015dadb9ebe83 (patch)
tree04a9ce1bceb5e5c4d0a715eda0ca9689ac424c58 /src/theory/quantifiers/quant_split.cpp
parentca1b17c8bba3681643a1a3de19d32b038c38aceb (diff)
Minor changes to sep logic, epr, quantifier splitting.
Diffstat (limited to 'src/theory/quantifiers/quant_split.cpp')
-rw-r--r--src/theory/quantifiers/quant_split.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 5aff1a848..35b3e1f9e 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -48,7 +48,7 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
}else{
int score = -1;
if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
- score = dt.isInterpretedFinite() ? 1 : -1;
+ score = dt.isInterpretedFinite() ? 1 : 0;
}else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
score = dt.isInterpretedFinite() ? 1 : -1;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback