diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index daa595302b8300465e6be56e2f6aee1b0b33ea7f..95d6eb149d7f9ad7f48b075bfdd4f6264d0b493f 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -40,6 +40,8 @@ import de.prob.animator.domainobjects.AbstractEvalResult;
 import de.prob.animator.domainobjects.ClassicalB;
 import de.prob.animator.domainobjects.ErrorItem;
 import de.prob.animator.domainobjects.EvalElementType;
+import de.prob.animator.domainobjects.EvalExpandMode;
+import de.prob.animator.domainobjects.EvalOptions;
 import de.prob.animator.domainobjects.EvalResult;
 import de.prob.animator.domainobjects.EventB;
 import de.prob.animator.domainobjects.FormulaExpand;
@@ -149,6 +151,13 @@ public final class ProBKernel extends BaseKernel {
 	private static final @NotNull Pattern BSYMB_COMMAND_PATTERN = Pattern.compile("\\\\([a-z]+)");
 	private static final @NotNull Pattern LATEX_FORMULA_PATTERN = Pattern.compile("(\\$\\$?)([^\\$]+)\\1");
 	
+	public static final @NotNull EvalOptions EVAL_OPTIONS = EvalOptions.DEFAULT
+		.withProvideStoredLetValues(true)
+		.withEvalExpand(EvalExpandMode.EFFICIENT);
+	public static final @NotNull EvalOptions TRUNCATE_EVAL_OPTIONS = EVAL_OPTIONS
+		.withEvalExpand(EvalExpandMode.NEVER)
+		.withExpand(FormulaExpand.TRUNCATE);
+	
 	private static final @NotNull Collection<@NotNull Class<? extends Command>> COMMAND_CLASSES = Collections.unmodifiableList(Arrays.asList(
 		AssertCommand.class,
 		BrowseCommand.class,
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 9c974c0afcc9de2edd0f66ebda38d2379e6592d2..781d113846037b20d1a04a2d326613bea9fff022 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -72,7 +72,7 @@ public final class AssertCommand implements Command {
 		final ProBKernel kernel = this.kernelProvider.get();
 		final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.TRUNCATE);
 		final AbstractEvalResult result = CommandUtils.withSourceCode(formula, () -> 
-			kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+			kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.TRUNCATE_EVAL_OPTIONS))
 		);
 		if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
 			// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index ae399d3d5de98941bacd22c21924c0f7f5d1e4e8..0b2da0e4809dcfbcdb03c558f4bb3354618af90a 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -67,7 +67,7 @@ public final class EvalCommand implements Command {
 		final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
 		final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.EXPAND);
 		return CommandUtils.withSourceCode(formula, () -> {
-			final AbstractEvalResult aer = this.animationSelector.getCurrentTrace().evalCurrent(formula);
+			final AbstractEvalResult aer = this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.EVAL_OPTIONS);
 			return CommandUtils.displayDataForEvalResult(kernel.postprocessEvalResult(aer));
 		});
 	}
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index 84b288cddf975fc2440f08808be32da87fc67852..dc6c27230fa0fa7febaa2a47e775acf8d1cf2ef1 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -80,7 +80,7 @@ public final class LetCommand implements Command {
 		final ProBKernel kernel = this.kernelProvider.get();
 		final IEvalElement formula = kernel.parseFormula(expression, FormulaExpand.EXPAND);
 		final AbstractEvalResult evaluated = CommandUtils.withSourceCode(formula, () ->
-			kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+			kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.EVAL_OPTIONS))
 		);
 		if (evaluated instanceof EvalResult) {
 			kernel.getVariables().put(name, ((EvalResult)evaluated).getValue());