Project

General

Profile

Bug #5226

Fix unsupported op in CUF - unsignedbv

Added by Karine Even Mendoza almost 7 years ago. Updated almost 7 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Karine Even Mendoza
Start date:
31/05/2017
Due date:
% Done:

0%

Estimated time:

Description

(Cannot refine due to 1 unsupported operators;e.g., unsignedbv)

VERIFICATION FAILED
TOTAL TIME FOR CHECKING THIS CLAIM: 0.016

Checked Assertion:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/bitvector-regression/pointer_extension2_false-unreach-call.c line 19 function main
assertion
FALSE
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog$ ./hifrog --theoref --force ../../../../../../hi-bench/challenge-bench/sv-comp16/c/bitvector-regression/pointer_extension2_false-unreach-call.c

History

#1 Updated by Karine Even Mendoza almost 7 years ago

  • Status changed from New to Closed

fixed the print. Need to implement more operators in opensmt

Also available in: Atom PDF