Description
In my program, it sometimes happens that the connected external propagator is notified of a backtrack to level 0, then immeadiately after, it is notified of a backtrack to level 2. It is not notified of any new assignments or of a new decision level inbetween. This happens for me both with the main (1462073) and development (4b1a55d) branch on several of my instances. I don't really know how I could produce a minimal example of this.
I've tried following Cadical to see what happens inbetween the two backtracks. The first backtrack to level 0 happens in Internal::elim, in the call to backtrack ();right at the top.
Line 988 in 1462073
A few lines below,
subsume (update_limits); is called,Line 1007 in 1462073
which calls different vivify functions
Internal::vivify and Internal::vivify_round until in Internal::vivify_clause the function vivify_assume (-lit) is called,Line 853 in 1462073
which increases the internal level (in my cases it is called several times until the level is 3). This seems to not be communicated to the external propagator and in the next block, still in
Internal::vivify_clause, backtrack (level - 1); is called which does notify the external propagator of a backtrack to level 2.Line 901 in 1462073
I don't think this is the desired behaviour as we only want to backtrack to lower decision levels, and either the new levels should be communicated to the connected external propagator or the backtrack should not be communicated at that point?
It might be that something is very wrong in my code as well, but I thought it might be good for you to have a look whether there should actually be a notification to the external propgator in there; or you might have an idea what could go wrong in my code to cause Cadical to not notify in the right order.
I can get around this issue for me by faking the notifications with calling notify_new_decision_level() myself but I don't trust that this will not cause other problems.