# PVS Bug 481

Synopsis: (ASSERT :linear? T)
Severity: serious
Priority: medium
Responsible: shankar
State: open
Class: sw-bug
Arrival-Date: Wed Sep 6 12:00:01 2000
Originator: Bruno Dutertre
Organization: csl.sri.com
Release: PVS 2.3
Environment:
System:
Architecture:
Description:
Setting :linear? to T does no seem to have any effect
on what assert does, or is some kind of interaction
with flush?
For example,
assert_linear : THEORY
BEGIN
a, b, c, d: VAR nzreal
test: LEMMA a * b * (c / b) = d
END assert_linear
then
test :
|-------
{1} FORALL (a, b, c, d: nzreal): a * b * (c / b) = d
Rule? (skolem!)
Skolemizing,
this simplifies to:
test :
|-------
{1} a!1 * b!1 * (c!1 / b!1) = d!1
Rule? (assert :linear? T)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to:
test :
|-------
{1} (c!1 / b!1) * a!1 * b!1 = d!1
That can be annoying if you try to use a rewrite rule like
x * y * (z / y) = x * z
There's also a minor bug in the way auto-rewrite with antecedent
formulas work. If you have
(AUTO-REWRITE -1)
...
(AUTO-REWRITE -1)
in a proof branch, then show-auto-rewrites will show two rewrite
rules with the same name, even though formula -1 may not be the
same in the two cases.
Bruno
How-To-Repeat:
Fix: