Project

General

Profile

Actions
Copy link

Bug #5548

open

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

Added by Sepideh Asadi about 7 years ago. Updated about 7 years 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 1 (0 open — 1 closed)

Bug #5549: .Closed29/09/2017

Actions
Actions
Copy link
 #1

Updated by Sepideh Asadi about 7 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

Actions
Copy link

Also available in: Atom PDF