search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
360 stars 45 forks source link

fixes #400 #495

Closed ahmed-irfan closed 3 months ago

ahmed-irfan commented 4 months ago

MCSAT: purify the arguments of bv-array terms if they are arithmetic literals, i.e. a + b < 0.

coveralls commented 4 months ago

Coverage Status

coverage: 65.538% (+0.007%) from 65.531% when pulling 99590ec210dd1784f8940c99bc1f34c707223e15 on mcsat-bv-array-purify into 553897f5f339bc8852e104d0fa6a3ebb21e0a4d0 on master.