fix counterexample printing with assumes
MODIFY
ir/instr.h
ir/instr.h
@@ -300,7 +300,7 @@ class Assume final : public Instr {
bool if_non_poison; /// cond only needs to hold if non-poison
public:
Assume(Value &cond, bool if_non_poison)
- : Instr(Type::voidTy, ""), cond(cond), if_non_poison(if_non_poison) {}
+ : Instr(Type::voidTy, "assume"), cond(cond), if_non_poison(if_non_poison) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;

MODIFY
ir/state_value.h
ir/state_value.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "smt/expr.h"
+#include <ostream>
#include <utility>
#include <vector>

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -618,15 +618,15 @@ public:
auto op_name = to_string(op / 2);
auto l = make_unique<ICmp>(*int_types[1].get(),
- "$range_l$" + op_name + value_name(llvm_i),
+ "%range_l#" + op_name + value_name(llvm_i),
ICmp::SGE, i, *get_operand(low));
auto h = make_unique<ICmp>(*int_types[1].get(),
- "$range_h$" + op_name + value_name(llvm_i),
+ "%range_h#" + op_name + value_name(llvm_i),
ICmp::SLT, i, *get_operand(high));
auto r = make_unique<BinOp>(*int_types[1].get(),
- "$range$" + op_name + value_name(llvm_i),
+ "%range#" + op_name + value_name(llvm_i),
*l.get(), *h.get(), BinOp::And);
auto r_ptr = r.get();

fix counterexample printing with assumes