27   auto B = Ctx.atom();  in TEST()
37   auto B = Ctx.neg(Ctx.atom());  in TEST()
47   auto B = Ctx.conj(Ctx.atom(), Ctx.atom());  in TEST()
58   auto B = Ctx.disj(Ctx.atom(), Ctx.atom());  in TEST()
69   auto B = Ctx.impl(Ctx.atom(), Ctx.atom());  in TEST()
80   auto B = Ctx.iff(Ctx.atom(), Ctx.atom());  in TEST()
91   auto B0 = Ctx.atom();  in TEST()
92   auto B1 = Ctx.atom();  in TEST()
111       Ctx.atom(),  in TEST()
112       Ctx.disj(Ctx.atom(),  in TEST()
113                Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));  in TEST()
130   auto True = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
140   auto Cond = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
141   auto Then = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
142   auto Else = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
167   auto True = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
168   auto False = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
169   auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));  in TEST()
190   auto X = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
191   auto Y = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
216   std::vector<BoolValue *> Constraints({Ctx.atom()});  in TEST()
234   auto B0 = Ctx.atom();  in TEST()
255   std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});  in TEST()
276   auto B0 = Ctx.atom();  in TEST()
277   auto B1 = Ctx.atom();  in TEST()
303   auto B0 = Ctx.atom();  in TEST()
304   auto B1 = Ctx.atom();  in TEST()
335   auto B0 = Ctx.atom();  in TEST()
336   auto B1 = Ctx.atom();  in TEST()
367   auto Cond = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
368   auto Then = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
369   auto Else = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
409   auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
410   auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
411   auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());  in TEST()