False possitive verification result

[lichye]

c432.zip
This is the example from ISCAS85 Benchmark. This is the case c432.

I add property "assert property (0);" and this got verified. I assumed this must be denied.

The result is “Parsing c432.sv
Converting
Type-checking Verilog::c432
Using module 'c432'
using default bound 1
Generating Decision Problem
Using MiniSAT 2.2.1 with simplifier
Properties
Solving with propositional reduction
SAT checker: instance is UNSATISFIABLE
UNSAT: No path found within bound

** Results:
[c432.assert.1] always 0: PROVED up to bound 10”