Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1054


Synopsis:        Translation of unary minus to Yices
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Fri Apr 23 01:10:00 -0700 2010
Originator:      Johannes Eriksson
Release:         PVS 4.2
Organization:    abo.fi
Environment: 
 System:          
 Architecture: 

Description: 
  It seems like the translation of unary minus to Yices is
  incorrect. "-x" is currently translated into "(- x), which is
  interpreted as identity in Yices, as per the following FAQ entry:
  
  http://yices-wiki.csl.sri.com/index.php/FAQ#Why_is_.28-_10.29_equal_to_10_.3F
  
  Due to the mistranslation, (yices) proves, e.g., the following goal:
  
  l1 :
  
    |-------
  {1}   -1 > 0
  
  Rule? (yices)
  ydefns =
  
  yforms =
   (assert (not (>  (-  1) 0)))
  
  Result = unsat
  Logical context is inconsistent. Use (reset) to reset.
  unsat
  Statistics:
  num. decisions:                   0
  num. conflicts:                   1
  num. bool vars:                   0
  memory used:                      6.10938 Mb
  cpu time:                         0.014997 secs
  
  Yices translation of negation is unsatisfiable
  Simplifying with Yices,
  Q.E.D.
  
  
  Regards,
  Johannes

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools