Project

General

Profile

Actions
Copy link

Bug #10880

closed

Try to set counterexample.export.allowImpreciseCounterexamples=false

Added by Evgeny Novikov over 3 years ago. Updated over 3 years ago.

Status:
Closed
Priority:
High
Assignee:
Evgeny Novikov
Category:
Preset jobs, marks and tags
Target version:
3.2
Start date:
07/07/2021
Due date:
% Done:

0%

Estimated time:
Detected in build:
git
Platform:
Published in build:

Description

A long ago counterexample.export.allowImpreciseCounterexamples was supported and set to true in the ldv-bam configuration. Nowadays, it seems to result just in failures of RP:

KeyError: 'Entry node has not been set yet'

since nobody cares to provide imprecise violation witnesses. Thus, I will try to switch this option off.

Actually Anton Vasiliev investigated this option and its behavior.

Actions
Copy link
 #1

Updated by Evgeny Novikov over 3 years ago

  • Status changed from New to Resolved

I fixed the issue in branch disable-imprecise-counterexamples that undergoes testing right now.

Actions
Copy link
 #2

Updated by Evgeny Novikov over 3 years ago

  • Status changed from Resolved to Closed

As expected, tests passed, so, I merged the branch to master in 0a157f8ac.

Actions
Copy link

Also available in: Atom PDF