| 1510 | } |
| 1511 | |
| 1512 | void TypingAssignments::operator++(void) { |
| 1513 | if (has_only_one_solution) { |
| 1514 | is_unsat = true; |
| 1515 | } else { |
| 1516 | EnableSMTQueriesTMP tmp; |
| 1517 | s.block(r.getModel(), &sneg); |
| 1518 | r = s.check("typing"); |
| 1519 | assert(r.isSat() || r.isUnsat()); |
| 1520 | } |
| 1521 | } |
| 1522 | |
| 1523 | TypingAssignments TransformVerify::getTypings() const { |
| 1524 | auto c = t.src.getTypeConstraints() && t.tgt.getTypeConstraints(); |