Skip to content

Commit

Permalink
abstRefineArith -> abstRefineArithmetic
Browse files Browse the repository at this point in the history
  • Loading branch information
msooseth committed Sep 4, 2023
1 parent 0f51fe8 commit 02ea2e4
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions cli/cli.hs
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ data Command w
, smttimeout :: w ::: Maybe Natural <?> "Timeout given to SMT solver in seconds (default: 300)"
, maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point"
, loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
, abstractArithmetic :: w ::: Bool <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
, abstractArithmetic :: w ::: Bool <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
, abstractMemory :: w ::: Bool <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
, askSmtIterations :: w ::: Integer <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
}
Expand Down Expand Up @@ -216,7 +216,7 @@ equivalence cmd = do
, maxIter = cmd.maxIterations
, askSmtIters = cmd.askSmtIterations
, loopHeuristic = cmd.loopDetectionHeuristic
, abstRefineArith = cmd.abstractArith
, abstRefineArith = cmd.abstractArithmetic
, abstRefineMem = cmd.abstractMemory
, rpcInfo = Nothing
}
Expand Down Expand Up @@ -303,7 +303,7 @@ assert cmd = do
maxIter = cmd.maxIterations,
askSmtIters = cmd.askSmtIterations,
loopHeuristic = cmd.loopDetectionHeuristic,
abstRefineArith = cmd.abstractArith,
abstRefineArith = cmd.abstractArithmetic,
abstRefineMem = cmd.abstractMemory,
rpcInfo = rpcinfo
}
Expand Down

0 comments on commit 02ea2e4

Please sign in to comment.