Z3 TAR implementation has wrong answers

Bug #1870506 reported by Peter Gjøl Jensen
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
verifypn
New
Undecided
Peter Gjøl Jensen

Bug Description

The following list of models and queries from MCC'19-set yield wrong answers:

RefineWMG-PT-002-002-ReachabilityCardinality-13
RefineWMG-PT-002-003-ReachabilityCardinality-04
RefineWMG-PT-002-003-ReachabilityCardinality-06
RefineWMG-PT-002-003-ReachabilityCardinality-13
RefineWMG-PT-005-005-ReachabilityCardinality-15
RefineWMG-PT-007-007-ReachabilityCardinality-01
RefineWMG-PT-007-007-ReachabilityCardinality-06
RefineWMG-PT-007-008-ReachabilityCardinality-09
RefineWMG-PT-010-011-ReachabilityCardinality-00
RefineWMG-PT-015-015-ReachabilityCardinality-03
RefineWMG-PT-015-016-ReachabilityCardinality-10
RefineWMG-PT-025-025-ReachabilityCardinality-01
RefineWMG-PT-025-026-ReachabilityCardinality-07
RefineWMG-PT-100-100-ReachabilityCardinality-12

run with "-q 0 -tar -r 1 "

To post a comment you must log in.
This report contains Public information  
Everyone can see this information.

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.