title: Specifying initial model values for Z3
body: <p>How to specify initial 'soft' values for the model? This initial model is the result of solving a similar query, and it is likely that this model has a correct pieces or even may be true for the current query.</p>
  
  <p>Currently I am simulating this with an incremental solving and <a href="https://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3">hard/soft constraints</a>:</p>
  
  <pre><code>(define-fun trans_assumed ((a Int)) Int
  ; an initial model, which may be (partially) true
  )
  
  (declare-fun trans_sought ((a Int)) Int) 
  
  (declare-const p Bool)
  (assert (=&gt; p (forall ((a Int)) (= (trans_assumed a) (trans_sought a)))))
  (check-sat p) ; in hope that trans_assumed values will be used as initial below
  
  ; add here the main constraints for trans_sought function
  
  (check-sat) ; Z3 will use trans_assumed as a starting point for trans_sought
  </code></pre>
  
  <p>Does this really specify initial values for <code>trans_sought</code> to be <code>trans_assumed</code>?</p>
  
  <p>Incremental mode of solving is slow compared to sequential. Any better ways of introducing initial values?</p>