On 22 Oct 2010, at 15:02, Vladimir Klebanov wrote:
Hi again,
one strange issue we have encountered relates to prover selection:
-Load the included example 0.8 (Bag.java)
-Fix the (intended) typo in the length attribute
-Choose verify with CVC3 (the included 32bit Linux version)
-Receive the errors included below
The strange thing is that the log says "using Simplify-1.5.4.linux"
even though I'm clicking the CVC3 button/menu item. At the same time
it is possible to verify other examples (e.g., 3.2.15) in the same
manner without complaints (though the logs there also say "using
simplify" even though I click on CVC3).
On 22 Oct 2010, at 15:02, Vladimir Klebanov wrote:
Hi again,
one strange issue we have encountered relates to prover selection:
-Load the included example 0.8 (Bag.java) -Fix the (intended) typo in the length attribute -Choose verify with CVC3 (the included 32bit Linux version) -Receive the errors included below
The strange thing is that the log says "using Simplify-1.5.4.linux" even though I'm clicking the CVC3 button/menu item. At the same time it is possible to verify other examples (e.g., 3.2.15) in the same manner without complaints (though the logs there also say "using simplify" even though I click on CVC3).