* changing the bitblast-eager to bitblast on pre-register

* changing the bitblast-eager to bitblast on pre-register
* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate)
* when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true)
* bitblast-eager implies decision=internal