diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-15 11:44:15 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-15 11:44:15 -0500 |
| commit | b3f716fc402e2508a2ae1183fcfebebd2c95d6a3 (patch) | |
| tree | e4b45bf7590bd005b85608498a54e866ef581d68 /src/theory | |
| parent | 213433866fd07e94d40909484ef1e906722cd0c7 (diff) | |
Fix bug 806. Minor fixes to remove term formula pass.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 84743fc1d..33dfa19bc 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -817,6 +817,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) { d_solution = s; const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); + Trace("csi-sol") << "Reconstruct to syntax " << s << ", allow all = " << dt.getSygusAllowAll() << " " << stn << ", reconstruct = " << rconsSygus << std::endl; //reconstruct the solution into sygus if necessary reconstructed = 0; |