Add support for dumping of incremental SMT2 formulas.

[aniemetz]

Currently, the SMT2 dumper does not fully support dumping of incremental formulas.

When boolector_dump_smt2 is called anytime while solving incrementally, it only dumps the current state of the input formula up to the first (check-sat) call without considering current assumptions/scopes. For example,

(set-logic QF_BV)
(set-option :incremental true)                                                  
(declare-const y (_ BitVec 2))                                                  
(define-fun f ((x (_ BitVec 2))) (_ BitVec 2) (bvadd x #b01))
(assert (distinct (f y) #b10))
(check-sat)
(push 1)                                                                        
(assert (= (f y) #b10))
(pop 1)                                                                         
(assert (= (f y) #b10))
(check-sat)

prints

(set-logic QF_BV)
(declare-fun y () (_ BitVec 2))
(define-fun f ((_f_x (_ BitVec 2))) (_ BitVec 2)
(bvadd _f_x #b01))
(assert 
 (not 
  (= #b10 
   (f y))))
(check-sat)
(exit)

Removing the (check-sat) call is added before the first push yields

(set-logic QF_BV)
(assert false)
(check-sat)
(exit)