Skip to content

Commit

Permalink
Merge pull request #790 from pieter-bos/condition-exp
Browse files Browse the repository at this point in the history
symbexlog: fix conditionExp for big and/or
  • Loading branch information
marcoeilers authored Jan 21, 2024
2 parents 34062b3 + 527932b commit 093361e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/main/scala/rules/Evaluator.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1619,7 +1619,7 @@ object evaluator extends EvaluationRules {
case `stop` => Q(s1, t0, v1) // Done, if last expression was true/false for or/and (optimisation)
case _ =>
joiner.join[Term, Term](s1, v1)((s2, v2, QB) =>
brancher.branch(s2.copy(parallelizeBranches = false), t0, Some(viper.silicon.utils.ast.BigAnd(exps)), v2, fromShortCircuitingAnd = true) _ tupled swapIfAnd(
brancher.branch(s2.copy(parallelizeBranches = false), t0, Some(exps.head), v2, fromShortCircuitingAnd = true) _ tupled swapIfAnd(
(s3, v3) => QB(s3.copy(parallelizeBranches = s2.parallelizeBranches), constructor(Seq(t0)), v3),
(s3, v3) => evalSeqShortCircuit(constructor, s3.copy(parallelizeBranches = s2.parallelizeBranches), exps.tail, pve, v3)(QB))
){case Seq(ent) =>
Expand Down

0 comments on commit 093361e

Please sign in to comment.