Project

General

Profile

Actions
Copy link

Bug #6932

open

Internal Assertion failure for ddv.c

Added by Sepideh Asadi over 6 years ago. Updated over 6 years ago.

Status:
Resolved
Priority:
Normal
Assignee:
-
Start date:
24/03/2018
Due date:
% Done:

0%

Estimated time:

Description

./hifrog --logic qfuf --claim 1 ./testcases/ddv.c

it happens in qflra as well.

Error:
Assertion failed: ("Error: using non-SSA symbol in the SMT encoding" && (is_L2_symbol || is_nil_or_symex)), function extract_expr_str_name, file ...trunk/cprover/src/funfrog/solvers/smtcheck_opensmt2.cpp, line 630.
Abort trap: 6

Files

Screen Shot 2018-03-24 at 18.22.28.png (97.2 KB) Screen Shot 2018-03-24 at 18.22.28.png Sepideh Asadi, 24/03/2018 18:25
Actions
Copy link
 #1

Updated by Martin Blicha over 6 years ago

In current version, I get no assertion violation.
Is this still actual?

Actions
Copy link
 #2

Updated by Martin Blicha over 6 years ago

  • Status changed from New to Resolved

This has been fixed already.

Actions
Copy link

Also available in: Atom PDF