title: Finding the weakest precondition using z3py
body: <p>I want to find the weakest precondition given an action and post condition using z3py.</p>
  
  <p>Given the action <code>N = N + 1</code> and the post condition <code>N == 5</code> the weakest precondition would be N == 4.</p>
  
  <p>Using the Tactic <code>solve-eqs</code> this approach works for some post conditions but not others.
  When using the post condition <code>N &lt; 5</code> I get <code>[[Not(4 &lt;= N)]]</code>.</p>
  
  <p>But when using <code>N == 5</code> I get <code>[[]]</code>, when I would like <code>N == 4</code>.</p>
  
  <pre><code>N2 = Int('N2') # N after the action
  N = Int('N') # N before the action
  
  weakestPreconditionGoal = Goal()
  
  # 'N2 == n + 1' action
  # 'N2 == 5' post condition. 
  weakestPreconditionGoal.add(N2 == N + 1,  N2 == 5)
  
  t = Tactic('solve-eqs')
  wp = t(weakestPreconditionGoal)
  print(wp)
  </code></pre>
  
  <p>Is this the best approach find the weakest precondition?</p>
  
  <p>I have tried a several methods but am new to Z3 and can not figure out what approach to take or how to implement it.</p>