Bug #4679
VERIFICATION FAILED for /main-bench/TACAS17_ex/ex1_lra.c
100%
Description
./hifrog ~/dev/hi-bench/main-bench/TACAS17_ex/ex1_lra.c --claim 1 --logic qflra
Violated assertion at:
file "/home/sepid/dev/hi-bench/main-bench/TACAS17_ex/ex1_lra.c",
function "main",
line 20:
a >= 0
VERIFICATION FAILED
A real bug found.
Initial unwinding bound: 4294967295
Total number of steps: 1
Unwinding depth: 1 (2)
History
#1 Updated by Sepideh Asadi about 7 years ago
./hifrog ~/dev/hi-bench/main-bench/TACAS17_ex/ex1_lra.c --claim 1 --logic prop
ex1_lra.c also fails in propositional logic.
#2 Updated by Sepideh Asadi about 7 years ago
- Subject changed from VERIFICATION FAILED to VERIFICATION FAILED for /main-bench/TACAS17_ex/ex1_lra.c
#3 Updated by Karine Even Mendoza about 7 years ago
- Assignee set to Karine Even Mendoza
- % Done changed from 0 to 50
The original benchmark is:
unsigned int nondetUInt();
int sum ()
{
int s=0;
unsigned n;
for (int i = 0; i <1000; i++)
{
n = nondetUInt();
s=s+n;
}
return s;
}
int main()
{
int a,b,c;
a=sum();
assert(a>=0);b=sum();
assert(b>=0);c=a+b;
assert(c>=0);
}The lra version return UNSAT, use this command: ./../hifrog_theory_ref/hifrog/trunk/cprover/src/funfrog/hifrog main-bench/TACAS17_ex/ex1_lra.c --claim 1 --logic qflra --type-constraints 1
In prop, not sure if possible. Help? someone remember what we wanted to do here?
#4 Updated by Karine Even Mendoza about 7 years ago
- % Done changed from 50 to 100
seems to be just fine now
#5 Updated by Karine Even Mendoza about 7 years ago
- Status changed from New to Closed