[IPASIR UP] Search with uninitialized search limits

[Dekker1]

When implementing a lazy solving approach, I ended up in a situation where Cadical (with the IPASIR UP interface) would start with an empty formula, where the check_model callback in the ExternalPropagator would then add the initial clauses. Although this callback proceeded correctly, Cadical would then immediately return the “unknown” result.

I managed to trace this back to Cadical checking the search limits in the extended CDCL loop, and because its limits weren't initialized would immediately exit. I found that ensuring that the limits always get initialized when having an external propagator in Internal::solve seems to solve a problem.

I’ve attached a patch with this small change and an additional assertion that limits are initialized when checked. I’d love to hear whether this is the correct approach, or whether I’m overlooking something.

ipasirup_init_limits-1.patch

[m-fleury]

The general idea of the interface is that you add the initial clauses before asking cadical to solve the problem (instead of adding them during the check_model).

But we should fix this, thanks for reporting.

@kfazekas is mobical able to generate such problems (so empty and only adding clauses during check_model)?