From: Lutz Donnerhacke <lutz@iks-jena.de>
Subject: [Spark] Splitting 'and' conditions into multiple conditions
Date: Tue, 25 Mar 2003 21:48:33 +0000 (UTC)
Date: 2003-03-25T21:48:33+00:00 [thread overview]
Message-ID: <slrnb81jlh.7pb.lutz@belenus.iks-jena.de> (raw)
The simplifier is often unable to prove easy conclusions, because conditions
given als assert, precondition, and postcondition occur as a single
conclusion.
Example:
C1: res__1 >= buf__first and res__1 <= buf__last and (res__1 >= 0 and res__1
<= 0) -> res__1 >= buf__first and res__1 <= buf__last .
Or do I misinterpret this line containing an implication?
Should the simplifier not able to handle this by transfering the frist part
to the hypothis?
next reply other threads:[~2003-03-25 21:48 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-03-25 21:48 Lutz Donnerhacke [this message]
2003-03-26 9:41 ` [Spark] Splitting 'and' conditions into multiple conditions Peter Amey
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox