Project

General

Profile

Bug #7275

supposed be UNSAT, but it is SAT

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

Status:
New
Priority:
Normal
Assignee:
-
Start date:
06/05/2018
Due date:
% Done:

0%

Estimated time:

Description

file:
/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.

how to run?
./hifrog --logic prop --unwind 10
or --sum-theoref

query1 (678 KB) query1 Karine Even Mendoza, 08/05/2018 12:29

History

#1 Updated by Karine Even Mendoza 12 months ago

The problem is in propositional logic, we get SAT and not UNSAT
The SSA encoding is valid and gives UNSAT in z3, not sure where is the problem.
I attached the SSA dump here.

How can we get a dump from OpenSMT to test what is the input to OpenSMT?

Also available in: Atom PDF