Project

General

Profile

Bug #7805

UFInterpolator.C

Added by Sepideh Asadi 6 months ago. Updated 6 months ago.

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

0%


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.

sumth60.c Magnifier (793 Bytes) Sepideh Asadi, 29/08/2018 13:03

__preq_query_default_1.smt2 (9.78 KB) Sepideh Asadi, 29/08/2018 13:42

History

Also available in: Atom PDF