Project

General

Profile

Actions
Copy link

Bug #7275

open

supposed be UNSAT, but it is SAT

Added by Sepideh Asadi over 6 years ago. Updated over 6 years 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

Files

query1 (678 KB) query1 Karine Even Mendoza, 08/05/2018 12:29
Actions
Copy link
 #1

Updated by Karine Even Mendoza over 6 years 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?

Actions
Copy link

Also available in: Atom PDF