Prove that the sum of a list of negative numbers is negative

test_negative_list_sum.py

from z3 import *

def test_negative_list_sum():
  ll = Datatype('ll')
  ll.declare('empty')
  ll.declare('cons', ('car', IntSort()), ('cdr', ll))
  ll = ll.create()
  list_sum = Function('list_sum', ll, IntSort(), BoolSort())
  a,e = Consts('a e', ll)
  b,c,d = Ints('b c d')
  
  fp = Fixedpoint()
  fp.declare_var(a,b,c,d,e)
  fp.register_relation(list_sum)
  fp.rule(list_sum(a, 0), a == ll.empty)
  fp.rule(list_sum(a, d), [a != ll.empty, b < 0, ll.cons(b, e) == a, list_sum(e, c), b + c == d])
  assert fp.query(And(list_sum(a, b), a != ll.empty, b < 0)) == sat
  assert fp.query(And(list_sum(a, b), a != ll.empty, b >= 0)) == unsat