Fixed two bugs: the first one was related with variable elimination, the second one was related on learning from checker.
Minor on trace.