title: z3 with SMTlib2 input
body: <p>I just upgraded z3 from 4.1 to 4.3.1, and it seems that the smtlib2 input has changed :
  now, a function/constant declaration is not deleted by a pop statement.</p>
  
  <p>Here is the SMTlib2 input that works fine with z3 4.1 (and other SMT solvers...), but return with an  error with z3 4.3.1 : (error "line 19 column 25: invalid declaration, constant 'bs_2' (whith the given signature) already declared")</p>
  
  <pre><code>(set-option :produce-models true)
  (set-option :produce-unsat-cores true)
  (set-option :interactive-mode true)
  (set-option :print-success false)
  (push 1)
  (declare-fun bs_1 () Bool)
  (push 1)
  (declare-fun bs_2 () Bool)
  (assert (and  bs_1 (not bs_2)))
  (check-sat)
  (pop 1)
  (push 1)
  (declare-fun bs_2 () Bool)
  (assert (and  bs_1 (not bs_2)))
  (check-sat)
  (pop 1)
  (pop 1)
  (exit)
  </code></pre>
  
  <p>Removing the last bs_2 declaration works fine with z3 4.3.1, but not for z3 4.1.
  Am I using the push/pop wrong ?</p>