Project

General

Profile

Actions
Copy link

Bug #7805

open

UFInterpolator.C

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

Status:
New
Priority:
Normal
Assignee:
Sepideh Asadi
Start date:
29/08/2018
Due date:
% Done:

0%

Estimated time:

Description

File: sumth60.c (attached)

How to run:
--logic qfuf --claim 2

Error message:
RESULT: UNSAT - it holds!
Start generating interpolants...
Assertion failed: (!sorted_edges.empty( ) || tmp.back( )->target == x), function getSortedEdges, file /Users/sepidehasadi/2phd/dev/opensmt2/src/tsolvers/egraph/UFInterpolator.C, line 2451.

Files

Download all files
sumth60.c (793 Bytes) sumth60.c Sepideh Asadi, 29/08/2018 13:03
__preq_query_default_1.smt2 (9.78 KB) __preq_query_default_1.smt2 Sepideh Asadi, 29/08/2018 13:42
Actions
Copy link

Also available in: Atom PDF