tests/model/fp · dolmen · Tangled

forked from gbury/dolmen

dolmen tests model fp

29 files

Guillaume Bury · Fix newline issue in test · 3y ago

double_req_bl_0530a_true-unreach-call.c_1.expected

Fix bitv neg in the case of zero

double_req_bl_0530a_true-unreach-call.c_1.rsmt2

Fix bitv neg in the case of zero

double_req_bl_0530a_true-unreach-call.c_1.smt2

Fix bitv neg in the case of zero

Add test for fp size error

[Model] Add fp theory

integral.expected

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

min_max_bad_extension.expected

Model fixes (#151)

min_max_bad_extension.rsmt2

Model fixes (#151)

min_max_bad_extension.smt2

Model fixes (#151)

min_max.expected

Model fixes (#151)

Model fixes (#151)

Model fixes (#151)

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

small_fp.expected

Fix newline issue in test

Add test for fp size error

Add test for fp size error

to_ubv.expected

Fix to_ubv/sbv in models

Fix to_ubv/sbv in models

Fix to_ubv/sbv in models

toIntegral-has-solution-259.expected

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

toIntegral-has-solution-259.rsmt2

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

toIntegral-has-solution-259.smt2

Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

[Model] Add fp theory

[Model] Add fp theory

[Model] Add fp theory