Skip to content

Commit e6bc8f1

Browse files
committed
improve documentation
1 parent 69517ec commit e6bc8f1

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -287,8 +287,9 @@ private ITerm simplifyRational(ITerm pTerm) {
287287

288288
@Override
289289
protected @Nullable IExpression evalImpl(IExpression expr) {
290-
// TODO creating our own utility variables might eb unexpected from the user.
291-
// We might need to exclude such variables in models and formula traversal.
290+
// The utility variable only appears temporarily on the solver's stack.
291+
// The user should never notice it.
292+
// We might not even need an index/counter for the variable.
292293
String newVariable = "__JAVASMT__MODEL_EVAL_" + counter++;
293294

294295
// Extending the partial model does not seem to work in Princess if the formula uses rational

0 commit comments

Comments
 (0)