diff options
| author | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-09 23:36:32 +0200 |
|---|---|---|
| committer | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-13 18:25:43 +0200 |
| commit | 2e3c2464ca3522fe0a6dfc93ea36c88cbe7bf117 (patch) | |
| tree | bad98ff1c69a4e53c17324844c01771627a6d889 /sparsec | |
| parent | 0b0805cf17aeb6a6cd0a7ed3f47ad8f0b4a3407b (diff) | |
| download | sparse-dev-2e3c2464ca3522fe0a6dfc93ea36c88cbe7bf117.tar.gz | |
scheck: support pre-conditions via __assume()
A lot of simplifications are only valid when their variables
satisfy to some conditions (like "is within a given range" or
"is a power of two").
So, allow to add such pre-conditions via new _assume() statements.
Internally, all such preconditions are ANDed together and what is
checked is they imply the assertions:
AND(pre-condition) implies assertion 1
...
Note: IIUC, it seems that boolector has a native mechanism for such
things but I'm not sure if t can be used here.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
Diffstat (limited to 'sparsec')
0 files changed, 0 insertions, 0 deletions