title: Non-termination for soft constraints with strings using z3-4.8.14
body: <p>I've been experimenting with soft constraints (MAX-SMT formulas) using string theory. Using the latest version of Z3, I've encountered an issue related to the following formula.</p>
  <pre><code>(set-option :random-seed 0)
  (set-option :produce-models true)
  (set-option :produce-unsat-cores true)
  (set-info :status sat)
  
  (declare-fun t () String)
  (declare-fun t_fresh () String)
  (declare-fun s () String)
  (declare-fun s1 () String)
  (declare-fun s3 () String)
  
  (assert-soft  (and (= (str.at t 0) t_fresh) (= (str.len t) 1)) :weight 101 :id obj1)
  (assert-soft  (and (not (= (str.contains s t) true)) (= (str.++ s1 t_fresh s3) s)) :weight 100 :id obj1)
  (check-sat)
  
  (get-value (s1 s3 t_fresh s t ))
  (get-info :reason-unknown)
  (get-objectives)
  </code></pre>
  <p>Only by interrupting, Z3 returns a correct model and an interval:</p>
  <pre><code>((s1 &quot;&quot;)
   (s3 &quot;&quot;)
   (t_fresh &quot;A&quot;)
   (s &quot;&quot;)
   (t &quot;A&quot;))
  (:reason-unknown &quot;canceled&quot;)
  (objectives
   (obj1  (interval 0 100))
  )
  </code></pre>
  <p>Running each of the soft constraints by themselves, Z3 immediately returns the correct model and objectives for both.</p>
  <p>Note that each assertion by itself is satisfiable. The first assertion requires t and t_fresh to be equal, whereas the second assertion requires them to be different.</p>
  <p>I'm also wondering if there are any module parameters or other settings worth tweaking when dealing with MAX-SMT formulas?</p>
  <p>I already posted this issue on the issue tracker, however it seems like issues concerning the optimization module have less priority. I'm surprised to see this behavior with just two soft constraints and would therefore welcome a discussion.</p>