275       const Variable LeftSubVar = GetVar(&C->getLeftSubValue());  in buildBooleanFormula()  local
278       if (LeftSubVar == RightSubVar) {  in buildBooleanFormula()
282         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
283         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
291         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
293         Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
300       const Variable LeftSubVar = GetVar(&D->getLeftSubValue());  in buildBooleanFormula()  local
303       if (LeftSubVar == RightSubVar) {  in buildBooleanFormula()
307         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
308         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
316         Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
317         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
336       const Variable LeftSubVar = GetVar(&I->getLeftSubValue());  in buildBooleanFormula()  local
343       Formula.addClause(posLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
345       Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
351       const Variable LeftSubVar = GetVar(&B->getLeftSubValue());  in buildBooleanFormula()  local
354       if (LeftSubVar == RightSubVar) {  in buildBooleanFormula()
366         Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
367         Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
368         Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
369         Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()