Craig_TreeInterpolation for Camel

Heizmann · danieldietsch · commit fcec4fb1c790 · 2024-11-23T09:05:57.000+01:00
diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/strategy/CamelRefinementStrategy.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/strategy/CamelRefinementStrategy.java
@@ -59,7 +59,7 @@ public CamelRefinementStrategy(final StrategyFactory<L>.StrategyModuleFactory fa
 			createModules(final StrategyFactory<L>.StrategyModuleFactory factory) {
 
 		final List<IIpTcStrategyModule<?, L>> rtr = new ArrayList<>();
-		rtr.add(factory.createIpTcStrategyModuleSmtInterpolCraig(InterpolationTechnique.Craig_NestedInterpolation));
+		rtr.add(factory.createIpTcStrategyModuleSmtInterpolCraig(InterpolationTechnique.Craig_TreeInterpolation));
 		rtr.add(factory.createIpTcStrategyModuleZ3(InterpolationTechnique.FPandBPonlyIfFpWasNotPerfect));
 		return rtr.toArray(new IIpTcStrategyModule[rtr.size()]);
 	}

Original file line number	Diff line number	Diff line change
`@@ -59,7 +59,7 @@ public CamelRefinementStrategy(final StrategyFactory<L>.StrategyModuleFactory fa`
`59`	`59`	`createModules(final StrategyFactory<L>.StrategyModuleFactory factory) {`
`60`	`60`
`61`	`61`	`final List<IIpTcStrategyModule<?, L>> rtr = new ArrayList<>();`
`62`		`- rtr.add(factory.createIpTcStrategyModuleSmtInterpolCraig(InterpolationTechnique.Craig_NestedInterpolation));`
	`62`	`+ rtr.add(factory.createIpTcStrategyModuleSmtInterpolCraig(InterpolationTechnique.Craig_TreeInterpolation));`
`63`	`63`	`rtr.add(factory.createIpTcStrategyModuleZ3(InterpolationTechnique.FPandBPonlyIfFpWasNotPerfect));`
`64`	`64`	`return rtr.toArray(new IIpTcStrategyModule[rtr.size()]);`
`65`	`65`	`}`