From 3e74fe125685ddb594cf4848057ac59f69b97774 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 22 Apr 2015 15:12:22 +0200
Subject: [PATCH] Support InequalitySplit for Int32
---
src/main/scala/leon/synthesis/rules/InequalitySplit.scala | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 55e83bf40..02475d69d 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -14,7 +14,10 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory)
- val candidates = p.as.filter(_.getType == IntegerType).combinations(2).toList.filter {
+ val argsPairs = p.as.filter(_.getType == IntegerType).combinations(2) ++
+ p.as.filter(_.getType == Int32Type).combinations(2)
+
+ val candidates = argsPairs.toList.filter {
case List(a1, a2) =>
val toValLT = implies(p.pc, LessThan(Variable(a1), Variable(a2)))
--
GitLab