Skip to content

Commit

Permalink
smt: fix some mkIf typos (#1442)
Browse files Browse the repository at this point in the history
* smt: fix some mkIf typos

I suspect these came from a too-smart IntelliJ find and replace
  • Loading branch information
dhalperi committed May 20, 2018
1 parent dad667b commit 1ced212
Show file tree
Hide file tree
Showing 4 changed files with 5 additions and 5 deletions.
Expand Up @@ -706,8 +706,8 @@ private BoolExpr environmentBlockingClause(Model m) {
}

/**
* Checks that a property is always true by seeing if the encoding is unsatisfiable. mkIf the
* model is satisfiable, then there is a counter example to the property.
* Checks that a property is always true by seeing if the encoding is unsatisfiable. If the model
* is satisfiable, then there is a counter example to the property.
*
* @return A VerificationResult indicating the status of the check.
*/
Expand Down
Expand Up @@ -93,7 +93,7 @@ public class SymbolicRoute implements IDeepCopy<SymbolicRoute> {

/*
* Copy constructor used to create the SSA form.
* To avoid changing values along different mkIf branches,
* To avoid changing values along different If branches,
* we must create a new copy of several variables that can change.
*/
SymbolicRoute(SymbolicRoute other) {
Expand Down
Expand Up @@ -881,7 +881,7 @@ private void updateSingleValue(TransferParam<SymbolicRoute> p, String variableNa

/*
* The [phi] function from SSA that merges variables that may differ across
* different branches of an mkIf statement.
* different branches of an If statement.
*/
private Pair<Expr, Expr> joinPoint(
TransferParam<SymbolicRoute> p,
Expand Down
Expand Up @@ -7,7 +7,7 @@
import java.util.Map;

/**
* A wrapper class that simplifies adding variables to the network model. mkIf debugging is enabled,
* A wrapper class that simplifies adding variables to the network model. If debugging is enabled,
* then it creates new variables to track the state of the other variables in the model. This allows
* the solver to create a minimal unsat core, which is useful for debugging.
*
Expand Down

0 comments on commit 1ced212

Please sign in to comment.