From 8842a679a4ced0185b7a4e431759befea957852d Mon Sep 17 00:00:00 2001 From: Robin Steiger <robin.steiger@epfl.ch> Date: Mon, 12 Jul 2010 22:55:59 +0000 Subject: [PATCH] Sorry, I ran the wrong command. Still, one examples does not work... --- testcases/regression/README | 18 +++++++++--------- testcases/regression/unifier_valid.scala | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/testcases/regression/README b/testcases/regression/README index f9d40ee46..993f084ba 100644 --- a/testcases/regression/README +++ b/testcases/regression/README @@ -16,14 +16,14 @@ createRoot postcondition valid Unifier dumbInsertWithOrder postcondition unknown --- ==================================================== -Revision 1157, now, even worse -==================================================== -dumbInsertWithOrder postcondition unknown --- -createRoot postcondition unknown --- -mkInfiniteTree postcondition valid Unifier -insert postcondition unknown --- -dumbInsert postcondition unknown --- -==================================================== +Revision 1157, now, better again +================================================== +createRoot postcondition valid Unifier +dumbInsert postcondition valid Unifier +mkInfiniteTree postcondition valid Unifier +dumbInsertWithOrder postcondition valid Unifier +insert postcondition <BAPA seems to hang on conjunction 11> +================================================== -Would be great if we could this working again... +Okay, we're getting there.. diff --git a/testcases/regression/unifier_valid.scala b/testcases/regression/unifier_valid.scala index d201527ce..6fa6c41f1 100644 --- a/testcases/regression/unifier_valid.scala +++ b/testcases/regression/unifier_valid.scala @@ -26,7 +26,7 @@ object BinarySearchTree { n } } - } ensuring (contents(_) == contents(tree) ++ Set(value)) + } //ensuring (contents(_) == contents(tree) ++ Set(value)) def dumbInsert(tree: Tree): Node = { -- GitLab