diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-17 09:23:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-17 09:23:14 -0500 |
| commit | 19ab3936ef46e93a98a142e0c454659ecc1d1e27 (patch) | |
| tree | 23c04865d859d43e65cdf89fcf427931e26158ee /src/theory/quantifiers/sygus/sygus_pbe.cpp | |
| parent | 13e248f4087347721c731c1f21a6f8b66dc52ed1 (diff) | |
Internal propagation for refinement lemmas (#1932)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index cd011ef44..9919dff49 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -31,7 +31,6 @@ namespace quantifiers { CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) { - d_tds = d_qe->getTermDatabaseSygus(); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); d_is_pbe = false; |