ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 60 forks source link

Fix z3 version checks #628

Closed facundominguez closed 1 year ago

facundominguez commented 1 year ago

We were comparing 4.11.2 with 4.3.2 by comparing ["4", "11", "2"] >= ["4", "3", "2"]

Which would return False because "11" >= "3" is false.

This patch changes this to read the version components as integers instead of strings.

Tested with z3-4.11.0.

ranjitjhala commented 1 year ago

Wow thank you!!!