title: How to add new constraint for existing declared function in z3 using c++?
body: <p>I would like to know is there any way to add some new constraints for existing declared variables in the solver without getting the model.</p>
  
  <p>For example, if I have 2 declare functions:</p>
  
  <pre><code>(declare-fun k!648 () (_ BitVec 8))
  (declare-fun k!647 () (_ BitVec 8))
  </code></pre>
  
  <p>and some constraint with it.</p>
  
  <p>How can I get their declared names generally?</p>
  
  <p>The situation is that I want to add more constraints for the existing "variables?" in the constraint and solver them together. But I am confused about how to get existing "variables?" and then form the new constraint which is also correct for the solver.</p>