Project

General

Profile

Bug #5548

in Lattice: supposed to be SAT, but the lattice gives

Added by Sepideh Asadi over 1 year ago. Updated over 1 year ago.

Status:
New
Priority:
Low
Assignee:
-
Start date:
29/09/2017
Due date:
% Done:

100%

Estimated time:
(Total: 0.00 h)

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

Bug #5549: .Closed

History

#1 Updated by Sepideh Asadi over 1 year 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

Also available in: Atom PDF