Note: currently this PR only includes the positive case. The negative case is still pending.
All of the main assumptions should be present for the positive case to go through (assuming backend support). The main trick will be adding additional uninterpreted functions to prevent the backend from crashing with DecidePredicateUnknown.
Note: currently this PR only includes the positive case. The negative case is still pending.
All of the main assumptions should be present for the positive case to go through (assuming backend support). The main trick will be adding additional uninterpreted functions to prevent the backend from crashing with
DecidePredicateUnknown
.Fixes: #248