Project

General

Profile

Bug #5326

Seg fault when using slt with eq.

Added by Karine Even Mendoza almost 7 years ago.

Status:
New
Priority:
Normal
Assignee:
Antti Hyvärinen
Start date:
16/06/2017
Due date:
% Done:

0%

Estimated time:

Description

./hifrog ../../../../../../hi-bench/challenge-bench/sv-comp16/c/bitvector/soft_float_4_true-unreach-call.c.cil.c --theoref --bitwidth 64 --type-byte-constraints 2 --force --unwind 5

This code gets seg fault when try to make op: bvlogic->mkBVSgeq(args). If we set it to Sglt it works fine.

Here is the trace:

16133 Process terminating with default action of signal 11 (SIGSEGV)
16133 Access not within mapped region at address 0xF6633C8
16133 at 0x4F82AC2: Pterm::size() const (Pterm.h:234)
16133 by 0x4FDD9F9: BitBlaster::bbBvslt(PTRef) (BitBlaster.C:329)
16133 by 0x4FDD0CD: BitBlaster::bbTerm(PTRef) (BitBlaster.C:230)
16133 by 0x4FDD695: BitBlaster::bbEq(PTRef) (BitBlaster.C:294)
16133 by 0x4FDD09E: BitBlaster::bbTerm(PTRef) (BitBlaster.C:229)
16133 by 0x4FDCA04: BitBlaster::insert(PTRef, BVRef&) (BitBlaster.C:116)
16133 by 0x4FDCB95: BitBlaster::insertEq(PTRef, BVRef&) (BitBlaster.C:132)
16133 by 0x56C7DD: smtcheck_opensmt2t_cuf::refine_ce_one_iter(std::vector<exprt, std::allocator<exprt> >&, int) (in /home/karinek/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog/hifrog)

Any idea?

Also available in: Atom PDF