From f71faa8fbb0c15fb0f6d98a37a9ad97c0a863e83 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 26 Apr 2012 19:49:21 +0200
Subject: [PATCH] different sorting for VCs
---
src/main/scala/leon/Analysis.scala | 10 ++++------
1 file changed, 4 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 6458079be..25d3ac1fd 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -63,13 +63,11 @@ class Analysis(val program : Program, val reporter: Reporter = Settings.reporter
defaultTactic
}
- def vcSort(vc1: VerificationCondition, vc2: VerificationCondition) : Boolean = (vc1 < vc2)
-
if(funDef.body.isDefined) {
- allVCs ++= tactic.generatePreconditions(funDef).sortWith(vcSort)
- allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef).sortWith(vcSort)
- allVCs ++= tactic.generatePostconditions(funDef).sortWith(vcSort)
- allVCs ++= tactic.generateMiscCorrectnessConditions(funDef).sortWith(vcSort)
+ allVCs ++= tactic.generatePreconditions(funDef)
+ allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
+ allVCs ++= tactic.generatePostconditions(funDef)
+ allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
}
allVCs = allVCs.sortWith((vc1, vc2) => {
val id1 = vc1.funDef.id.name
--
GitLab