Bug #5548
in Lattice: supposed to be SAT, but the lattice gives
100%
Description
/hifrog --load-sum-model modlattice_model_lra --logic qflra --load-summaries __summaries_simple_mod_lra --no-itp --unwind 10 --claim 1 ../benchmarks/modulus_false-no-overflow.c
it includes bit-vector operators like a shift register. We should think of in the future to solve such issues with theoref
Subtasks
History
#1 Updated by Sepideh Asadi over 6 years ago
Sepideh Asadi wrote:
/hifrog --load-sum-model modlattice_model_lra --logic qflra --load-summaries __summaries_simple_mod_lra --no-itp --unwind 10 --claim 1 ../benchmarks/modulus_false-no-overflow.c
it includes bit-vector operators like a shift register. We should think of in the future to solve such issues with theoref
/hifrog --load-sum-model modlattice_model_lra --logic qflra --load-summaries __summaries_simple_mod_lra --no-itp --unwind 2 --claim 1 ../benchmarks/sanfoundry_24_false-valid-deref.c