diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-02 13:01:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-02 13:01:50 -0500 |
| commit | a84b54ea155251af6254237816e449589591b33c (patch) | |
| tree | 932321bb441693d7b2fc2539047db204ee2a097b /src/theory/uf | |
| parent | 9b9cd3a304f5830942a8b715b19e3cac0a771289 (diff) | |
Remove references to deprecated propagate as decision feature (#2258)
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 6161710f2..65f7238c9 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1172,9 +1172,6 @@ void SortModel::allocateCardinality( OutputChannel* out ){ } //require phase out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true ); - //add the appropriate lemma, propagate as decision - //Trace("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << " " << d_type << std::endl; - //out->propagateAsDecision( lem[0] ); d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality ); if( applyTotality( d_aloc_cardinality ) ){ |