Basic question about backjumping in SAT solvers
The intervening assignments between the current assignment and the backjump point might have been arrived at via considerable backtracking and backjumping themselves and it would be wasteful to repeat all that work.  But in the context of a modern solver that work may not need to be repeated, because:


Any conflicts that occurred during the intervening assignments should have produced conflict clauses that rule out those time-wasting bad assignments in the immediate future.
Some solvers implement "phase saving" which remembers whether a variable was assigned true or false across backjumps (and restarts).  So when DPLL chooses that variable again as a decision variable it will use the same true/false value, essentially picking up where it left off before the backjump.
The intervening assignments may not be repeated in the same order after the backjump.  Solvers have heuristics that decide which variable becomes the next decision variable.  These heuristics usually give preference to variables recently involved in conflicts, which usually has the effect of shuffling the decision variable order after every conflict.


There is another reason to backjump past 7 and then assert -3 and that is because of the way two-watched-literals works.  Two-watched-literals is a clever algorithm for noticing when clauses are made unit by an assignment.  It uses a lazy data structure that does not need to be updated for every clause referenced by an assignment and more importantly does not need to be updated at all when backtracking or backjumping.  You can assume every SAT solver that implements DPLL also uses this algorithm to track unit clauses.

But in order for the lazy data structure to work there are procedural rules that must be followed.  One of them is that you must roll back decision variable assignments and their unit propagations as a group.  So to use your example, if -3 were asserted after the 7 assignment instead of before it and the 7 assignment were ever rolled back, then the -3 assignment would be undone separate from the |6 1 2 assignments that caused it.  This would leave clause C, [-1 -2 -3], as a unit clause but two-watched-literals would not detect it.  DPLL search is now broken and the solver may be confused enough to later claim that it has a satisfying assignment when it doesn't.  If -3 is asserted together with the other consequences of the 6 assignment, then all the implications of that assignment will be rolled back together as they must be.