( Z3Py )объявление функции

Я хотел бы найти коэффициенты c и t в простой формуле «результат = x *t + c» для некоторых заданных пар результат / x:

from z3 import *

x=Int('x')
c=Int('c')
t=Int('t')

s=Solver()

f = Function('f', IntSort(), IntSort())

# x*t+c = result
# x, result = [(1,55), (12,34), (13,300)]

s.add (f(x)==(x*t+c))
s.add (f(1)==55, f(12)==34, f(13)==300)

t=s.check()
if t==sat:
    print s.model()
else:
   print t

... но результат явно неверный. Мне, вероятно, нужно узнать, как отображать аргументы функции.

Как правильно определить функцию?