Not all paths a found and some are listed multiple times

[zajer]

Before going into example I just want to emphesize that I have tinkered with the current code base to run it against the newest version of z3 (4.12.2) and python (3.11.4). To do so I have changed all occurences of inspect.getargspec to inspect.getfullargspec in symbolic/loader.py and symbolic/symbolic_types/symbolic_type.py

All tests except bignum are passing.

My example looks like the following:

def kolor(x,y):
  if y < x - 2 :
    return 7
  else :
    return 2

def zwierze(x,y):
  if y > 3 :
    return 10
  else:
    return 50

def czynnosc(x,y):
  if y < -x + 3 :
    return 100
  else :
    return 200

def yolo(a,b):
  return kolor(a,b)+zwierze(a,b)+czynnosc(a,b)

def expected_result():
  return [ 112, 157, 152, 217, 212, 257, 252]

#print (yolo(-2,4))

I have exected to find 7 paths with results like in the array returned by expected_result function but instead I got the following:

PyExZ3 (Python Exploration with Z3)
Exploring FILE.yolo
[('a', 0), ('b', 0)]
152
[('a', 8), ('b', 0)]
257
[('a', 0), ('b', 4)]
212
[('a', 0), ('b', 3)]
252
[('a', 8), ('b', 4)]
217
[('a', 0), ('b', -8)]
157
[('a', 8), ('b', 3)]
257
-------------------> FILE test failed <---------------------
Expected: {112: 1, 157: 1, 152: 1, 217: 1, 212: 1, 257: 1, 252: 1}, found: {152: 1, 257: 2, 212: 1, 252: 1, 217: 1, 157: 1}

Why am I getting 257 twice and why a path resulting in 112 is not found ?