Apply Dual Reduction after result is INF_OR_UNBD

teacher_base.py

@@ -125,6 +125,10 @@ class GurobiTeacherBase(TeacherBase):
     def check(self, candidate) -> z3.CheckSatResult:
         self._set_candidate(candidate)
         self._gp_model.optimize()
+        if self._gp_model.status == gp.GRB.INF_OR_UNBD:
+            self._gp_model.setParam("DualReductions", 0)
+            self._gp_model.optimize()
+
         if self._gp_model.status in [gp.GRB.OPTIMAL, gp.GRB.SUBOPTIMAL]:
             return z3.sat
         elif self._gp_model.status == gp.GRB.INFEASIBLE: