// Unit tests for the P-Code → Z3 encoder (encodePcodeFunction). Builds
// synthetic ir::pcode::Function inputs (no Ghidra, no r2) and runs them through
// the encoder + BinaryBBObserver, asserting the expected findings. This is the
// targeted regression coverage for the Z3 hazard hooks driven from P-Code.
#include <z3++.h>

#include <catch2/catch_test_macros.hpp>
#include <memory>
#include <string>
#include <vector>

#include "fold/binary/binary_bb_observer.hpp"
#include "fold/ir/pcode.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/pcode_encoder.hpp"

namespace {

using namespace fold::ir::pcode;

Varnode reg(std::uint64_t off, std::uint32_t size = 4) { return {Space::Register, off, size}; }
Varnode con(std::uint64_t val, std::uint32_t size = 4) { return {Space::Constant, val, size}; }

PcodeOp mk(Op op, Varnode out, std::vector<Varnode> in) {
    PcodeOp p;
    p.op = op;
    p.address = 0x1000;
    p.out = out;
    p.in = std::move(in);
    return p;
}
PcodeOp mkNoOut(Op op, std::vector<Varnode> in) {
    PcodeOp p;
    p.op = op;
    p.address = 0x1000;
    p.in = std::move(in);
    return p;
}
std::vector<fold::Finding> encode(const Function& fn) {
    std::vector<fold::Finding> out;
    auto ctx = std::make_shared<z3::context>();
    fold::binary::BinaryBBObserver obs(out, "test.bin", ctx);
    fold::symbolic::encodePcodeFunction(fn, *ctx, obs);
    return out;
}

bool hasDivByZero(const std::vector<fold::Finding>& fs) {
    for (const auto& f : fs)
        if (f.kind == fold::FindingKind::DivByZero)
            return true;
    return false;
}
bool hasNullDeref(const std::vector<fold::Finding>& fs) {
    for (const auto& f : fs)
        if (f.kind == fold::FindingKind::NullDeref)
            return true;
    return false;
}
bool hasBufferOverflow(const std::vector<fold::Finding>& fs) {
    for (const auto& f : fs)
        if (f.kind == fold::FindingKind::OOBAccess &&
            f.evidence.detector_name == "binary-buffer-overflow")
            return true;
    return false;
}

// Build a sink CALL: in[0] is the target address, in[1..] are the args.
// `buf_sizes` is parallel to `in` (index 0 = target, -1; arg i = in[i+1]).
PcodeOp mkCall(const std::string& callee, std::vector<Varnode> args,
               std::vector<std::int64_t> buf_sizes) {
    PcodeOp p;
    p.op = Op::Call;
    p.address = 0x1000;
    p.call_target = callee;
    p.in.push_back(con(0x2000, 8)); // target address
    for (auto& a : args)
        p.in.push_back(a);
    p.in_buffer_sizes = std::move(buf_sizes);
    return p;
}

Varnode uniq(std::uint64_t off, std::uint32_t size = 8) { return {Space::Unique, off, size}; }
// space-id const operand for LOAD/STORE (encoder ignores in[0]).
Varnode spaceId() { return con(1, 8); }

} // namespace

TEST_CASE("pcode-encoder: sdiv by a constant-zero divisor is division by zero", "[pcode][divz]") {
    // w9 = COPY const 0 ; tmp = INT_SDIV(w8, w9)
    Function fn;
    fn.name = "div0";
    fn.source = Source::Raw;
    fn.ops.push_back(mk(Op::Copy, reg(0x48), {con(0)}));
    fn.ops.push_back(mk(Op::IntSDiv, reg(0x100), {reg(0x40), reg(0x48)}));
    REQUIRE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: binary provenance preserves a full 64-bit address",
          "[pcode][provenance]") {
    Function fn;
    fn.name = "high_address_div0";
    auto div = mk(Op::IntSDiv, reg(0x100), {reg(0x40), con(0)});
    div.address = 0x1'0000'1000ULL;
    fn.ops.push_back(div);

    auto findings = encode(fn);
    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
    REQUIRE(findings[0].evidence.proof_mode == "binary-pcode-z3-heuristic");
    REQUIRE(findings[0].evidence.binary_vaddr == 0x1'0000'1000ULL);
    REQUIRE(findings[0].id.find("4294971392") != std::string::npos);
}

TEST_CASE("pcode-encoder: sdiv by a non-zero constant is not flagged", "[pcode][divz]") {
    Function fn;
    fn.name = "div5";
    fn.ops.push_back(mk(Op::Copy, reg(0x48), {con(5)}));
    fn.ops.push_back(mk(Op::IntSDiv, reg(0x100), {reg(0x40), reg(0x48)}));
    REQUIRE_FALSE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: zero divisor propagated through COPY chain is caught", "[pcode][divz]") {
    // w9 = COPY const 0 ; w10 = COPY w9 ; tmp = INT_SREM(w8, w10)
    Function fn;
    fn.name = "mod0";
    fn.ops.push_back(mk(Op::Copy, reg(0x48), {con(0)}));
    fn.ops.push_back(mk(Op::Copy, reg(0x50), {reg(0x48)}));
    fn.ops.push_back(mk(Op::IntSRem, reg(0x100), {reg(0x40), reg(0x50)}));
    REQUIRE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: full-register zero write is seen by a sub-register divisor read",
          "[pcode][divz]") {
    // Mirrors real ARM64 lifting: `mov w9,#0` zero-extends to x9, so the lifter
    // writes (reg X, size 8) = 0, but INT_SDIV reads the 4-byte sub-register
    // (reg X, size 4). The value map must alias them by offset.
    Function fn;
    fn.name = "div0_subreg";
    fn.ops.push_back(mk(Op::Copy, Varnode{Space::Register, 0x48, 8}, {con(0, 8)}));
    fn.ops.push_back(mk(Op::IntSDiv, reg(0x100), {reg(0x40), Varnode{Space::Register, 0x48, 4}}));
    REQUIRE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: divisor that is a fresh (unconstrained) input is not flagged",
          "[pcode][divz]") {
    // No definition of the divisor reg → fresh symbolic. The MVP gate fires
    // div-by-zero only for a provably-zero divisor, so a bare symbolic divisor
    // must NOT be reported (no FP on ordinary `a / b`).
    Function fn;
    fn.name = "divsym";
    fn.ops.push_back(mk(Op::IntSDiv, reg(0x100), {reg(0x40), reg(0x48)}));
    REQUIRE_FALSE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: raw div hazards are gated by real machine div addresses",
          "[pcode][divz]") {
    Function fn;
    fn.name = "artifact_div0";
    fn.source = Source::Raw;
    fn.machine_division_addresses_known = true;
    fn.machine_division_addresses = {0x2000};
    auto div = mk(Op::IntSDiv, reg(0x100), {reg(0x40), con(0)});
    div.address = 0x1000;
    fn.ops.push_back(div);
    REQUIRE_FALSE(hasDivByZero(encode(fn)));

    fn.ops.clear();
    div.address = 0x2000;
    fn.ops.push_back(div);
    REQUIRE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: fallthrough branch guard suppresses div-by-zero", "[pcode][divz]") {
    // if (den < 1) bail; num / den. CBRANCH is taken on the bad path, so the
    // fallthrough path reaching division has !(den < 1), which implies den != 0.
    Function fn;
    fn.name = "guarded_udiv";
    fn.source = Source::Raw;
    fn.machine_division_addresses_known = true;
    fn.machine_division_addresses = {0x2000};
    auto cmp = mk(Op::IntLess, uniq(0x200, 1), {reg(0x48), con(1)});
    cmp.address = 0x1000;
    fn.ops.push_back(cmp);
    auto br = mkNoOut(Op::CBranch, {con(0x3000, 8), uniq(0x200, 1)});
    br.address = 0x1004;
    fn.ops.push_back(br);
    auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), reg(0x48)});
    div.address = 0x2000;
    fn.ops.push_back(div);
    REQUIRE_FALSE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: fallthrough branch can prove symbolic divisor zero",
          "[pcode][divz][path]") {
    // if (den != 0) bail; num / den. The fallthrough path implies den == 0, so
    // the symbolic divisor is no longer a bare unconstrained input.
    Function fn;
    fn.name = "branch_proves_zero";
    fn.source = Source::Raw;
    fn.machine_division_addresses_known = true;
    fn.machine_division_addresses = {0x2000};
    auto cmp = mk(Op::IntNotEqual, uniq(0x200, 1), {reg(0x48), con(0)});
    cmp.address = 0x1000;
    fn.ops.push_back(cmp);
    auto br = mkNoOut(Op::CBranch, {con(0x3000, 8), uniq(0x200, 1)});
    br.address = 0x1004;
    fn.ops.push_back(br);
    auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), reg(0x48)});
    div.address = 0x2000;
    fn.ops.push_back(div);
    REQUIRE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: infeasible fallthrough prunes constant div-by-zero",
          "[pcode][divz][path]") {
    Function fn;
    fn.name = "infeasible_fallthrough";
    fn.source = Source::Raw;
    fn.machine_division_addresses_known = true;
    fn.machine_division_addresses = {0x2000};
    auto br = mkNoOut(Op::CBranch, {con(0x3000, 8), con(1, 1)});
    br.address = 0x1004;
    fn.ops.push_back(br);
    auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), con(0)});
    div.address = 0x2000;
    fn.ops.push_back(div);
    REQUIRE_FALSE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: taken block ordered next keeps taken-path hazard",
          "[pcode][divz][path]") {
    // if (den == 0) goto 0x2000; else return; 0x2000: num / den.
    // Some lifted streams place the taken target immediately after CBRANCH.
    // The encoder must not globally force the next op onto the fallthrough
    // (!cond) path and suppress this real taken-path division.
    Function fn;
    fn.name = "taken_next_has_hazard";
    fn.source = Source::Raw;
    fn.machine_division_addresses_known = true;
    fn.machine_division_addresses = {0x2000};
    auto cmp = mk(Op::IntEqual, uniq(0x200, 1), {reg(0x48), con(0)});
    cmp.address = 0x1000;
    fn.ops.push_back(cmp);
    auto br = mkNoOut(Op::CBranch, {con(0x2000, 8), uniq(0x200, 1)});
    br.address = 0x1004;
    fn.ops.push_back(br);
    auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), reg(0x48)});
    div.address = 0x2000;
    fn.ops.push_back(div);
    auto ret = mkNoOut(Op::Return, {});
    ret.address = 0x2004;
    fn.ops.push_back(ret);
    REQUIRE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: unconditional branch stops fallthrough hazards", "[pcode][divz][path]") {
    Function fn;
    fn.name = "branch_skips_hazard";
    fn.source = Source::Raw;
    fn.machine_division_addresses_known = true;
    fn.machine_division_addresses = {0x2000};
    auto branch = mkNoOut(Op::Branch, {con(0x3000, 8)});
    branch.address = 0x1000;
    fn.ops.push_back(branch);
    auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), con(0)});
    div.address = 0x2000;
    fn.ops.push_back(div);
    auto ret = mkNoOut(Op::Return, {});
    ret.address = 0x3000;
    fn.ops.push_back(ret);
    REQUIRE_FALSE(hasDivByZero(encode(fn)));
}

TEST_CASE("pcode-encoder: store-0-to-slot then load then deref is null-deref",
          "[pcode][nullderef]") {
    // Mirrors null_deref_direct lifting: addr = sp + 8 (recomputed identically),
    //   STORE(spaceid, sp+8, 0); ldr x8 = LOAD(spaceid, sp+8) -> 0;
    //   ldr w0 = LOAD(spaceid, x8) -> deref of 0.
    const Varnode sp = reg(0x20, 8);
    Function fn;
    fn.name = "nulld";
    fn.ops.push_back(mk(Op::IntAdd, uniq(0xc000), {sp, con(8, 8)}));
    fn.ops.push_back(mkNoOut(Op::Store, {spaceId(), uniq(0xc000), con(0, 8)}));
    fn.ops.push_back(mk(Op::IntAdd, uniq(0xc000), {sp, con(8, 8)}));
    fn.ops.push_back(mk(Op::Load, reg(0x48, 8), {spaceId(), uniq(0xc000)}));
    fn.ops.push_back(mk(Op::Load, reg(0x100, 4), {spaceId(), reg(0x48, 8)}));
    REQUIRE(hasNullDeref(encode(fn)));
}

TEST_CASE("pcode-encoder: deref of an ordinary stack slot is not null-deref",
          "[pcode][nullderef]") {
    // Load a (non-zero, unknown) value from sp+8 and deref it: sp+8 is not 0 and
    // the loaded value is fresh symbolic, so neither deref is reported.
    const Varnode sp = reg(0x20, 8);
    Function fn;
    fn.name = "nulld_neg";
    fn.ops.push_back(mk(Op::IntAdd, uniq(0xc000), {sp, con(8, 8)}));
    fn.ops.push_back(mk(Op::Load, reg(0x48, 8), {spaceId(), uniq(0xc000)}));
    fn.ops.push_back(mk(Op::Load, reg(0x100, 4), {spaceId(), reg(0x48, 8)}));
    REQUIRE_FALSE(hasNullDeref(encode(fn)));
}

// ── Stack buffer overflow ─────────────────────────────────────────

TEST_CASE("pcode-encoder: strcpy into a recovered finite buffer overflows", "[pcode][bof]") {
    // strcpy(dst, src) — unbounded; dst is a recovered 64-byte stack buffer.
    Function fn;
    fn.name = "bof_strcpy";
    fn.source = Source::SSA;
    fn.ops.push_back(mkCall("strcpy", {reg(0x0, 8), reg(0x8, 8)}, {-1, 64, -1}));
    REQUIRE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: strcpy with no recovered buffer size does not fire", "[pcode][bof]") {
    // No size recovered (raw stream / unrecovered local) -> FN, never FP.
    Function fn;
    fn.name = "bof_strcpy_nosize";
    fn.ops.push_back(mkCall("strcpy", {reg(0x0, 8), reg(0x8, 8)}, {-1, -1, -1}));
    REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: fgets with size larger than the buffer overflows", "[pcode][bof]") {
    // fgets(dst, 128, stream) into a 64-byte buffer: 128 > 64.
    Function fn;
    fn.name = "bof_fgets";
    fn.source = Source::SSA;
    fn.ops.push_back(mkCall("fgets", {reg(0x0, 8), con(128, 8), reg(0x8, 8)}, {-1, 64, -1, -1}));
    REQUIRE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: fgets with size equal to the buffer is safe", "[pcode][bof]") {
    // fgets(dst, 64, stream) into a 64-byte buffer: 64 == 64, not > cap.
    Function fn;
    fn.name = "fgets_ok";
    fn.source = Source::SSA;
    fn.ops.push_back(mkCall("fgets", {reg(0x0, 8), con(64, 8), reg(0x8, 8)}, {-1, 64, -1, -1}));
    REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: memcpy within the buffer bound is safe", "[pcode][bof]") {
    // memcpy(dst, src, 16) into a 64-byte buffer: 16 <= 64.
    Function fn;
    fn.name = "memcpy_ok";
    fn.source = Source::SSA;
    fn.ops.push_back(mkCall("memcpy", {reg(0x0, 8), reg(0x8, 8), con(16, 8)}, {-1, 64, -1, -1}));
    REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: read-only scanners are not buffer-copy sinks", "[pcode][bof]") {
    for (const std::string callee : {"memchr", "strchr", "strstr"}) {
        Function fn;
        fn.name = "scanner_" + callee;
        fn.source = Source::SSA;
        fn.ops.push_back(mkCall(callee, {reg(0x0, 8), reg(0x8, 8), con(128, 8)}, {-1, 64, -1, -1}));
        REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
    }
}

TEST_CASE("pcode-encoder: fortified chk wrappers are not modeled as unchecked copies",
          "[pcode][bof]") {
    Function fn;
    fn.name = "strncpy_chk_guarded";
    fn.source = Source::SSA;
    fn.ops.push_back(mkCall("strncpy_chk", {reg(0x0, 8), reg(0x8, 8), reg(0x10, 8), con(26, 8)},
                            {-1, 26, -1, -1, -1}));
    REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: non-sink call does not fire buffer overflow", "[pcode][bof]") {
    Function fn;
    fn.name = "call_printf";
    fn.source = Source::SSA;
    fn.ops.push_back(mkCall("printf", {reg(0x0, 8)}, {-1, 64}));
    REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: switch-state-machine dispatch reaches a case-body strcpy sink",
          "[pcode][switchvm][bof]") {
    // A switch-state-machine dispatch: the strcpy sink sits in a case body that
    // is only reachable through a Memory-space CBRANCH target (the SSA lifter
    // encodes branch targets in ram space and can fold the first instruction(s)
    // of a case body, so the target address differs from the case body's first
    // op address). An unconditional Branch separates the dispatch from the case
    // body, so the sink is NOT on the linear fallthrough path.
    Function fn;
    fn.name = "vm_dispatch";
    fn.source = Source::SSA;

    Varnode state = {Space::StackBase, 0x10, 4}; // dispatch state slot
    Varnode b1 = uniq(0x100, 1);
    Varnode b2 = uniq(0x101, 1);

    PcodeOp o0 = mk(Op::Copy, state, {con(0x41)});
    o0.address = 0x1000;
    PcodeOp o1 = mk(Op::IntEqual, b1, {state, con(0x41)});
    o1.address = 0x1001;
    PcodeOp o2 = mkNoOut(Op::CBranch, {Varnode{Space::Memory, 0x2000, 8}, b1});
    o2.address = 0x1002;
    PcodeOp o3 = mk(Op::IntEqual, b2, {state, con(0x93)});
    o3.address = 0x1003;
    PcodeOp o4 = mkNoOut(Op::CBranch, {Varnode{Space::Memory, 0x3000, 8}, b2});
    o4.address = 0x1004;
    // Default arm: unconditional jump past the case bodies — ends the linear
    // walk, so the strcpy below is only reachable via the dispatch CBRANCH.
    PcodeOp o5 = mkNoOut(Op::Branch, {Varnode{Space::Memory, 0x4000, 8}});
    o5.address = 0x1005;
    // Case body: the strcpy sink at address 0x3000 (the CBRANCH targets 0x3000 —
    // the folded `lea`), dst buffer recovered as 64 bytes.
    PcodeOp o6 = mkCall("strcpy", {reg(0x20, 8), reg(0x28, 8)}, {-1, 64, -1});
    o6.address = 0x3000;
    PcodeOp o7 = mkNoOut(Op::Return, {});
    o7.address = 0x3001;

    fn.ops = {o0, o1, o2, o3, o4, o5, o6, o7};
    REQUIRE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: raw stream does not follow Memory-space branch targets",
          "[pcode][switchvm][bof]") {
    // The raw stream encodes branch targets as Constant-space; Memory-space
    // targets (SSA-only) must NOT be followed in a raw-lifted function, so a
    // sink that sits behind a dispatch is unreachable in the raw lane.
    Function fn;
    fn.name = "vm_dispatch_raw";
    fn.source = Source::Raw;

    Varnode b1 = uniq(0x100, 1);
    Varnode b2 = uniq(0x101, 1);

    PcodeOp o0 = mk(Op::IntEqual, b1, {reg(0x0), con(0x41)});
    o0.address = 0x1000;
    PcodeOp o1 = mkNoOut(Op::CBranch, {Varnode{Space::Memory, 0x2000, 8}, b1});
    o1.address = 0x1001;
    PcodeOp o2 = mk(Op::IntEqual, b2, {reg(0x0), con(0x93)});
    o2.address = 0x1002;
    PcodeOp o3 = mkNoOut(Op::CBranch, {Varnode{Space::Memory, 0x3000, 8}, b2});
    o3.address = 0x1003;
    PcodeOp o4 = mkNoOut(Op::Branch, {Varnode{Space::Memory, 0x4000, 8}});
    o4.address = 0x1004;
    PcodeOp o5 = mkCall("strcpy", {reg(0x20, 8), reg(0x28, 8)}, {-1, 64, -1});
    o5.address = 0x3000;
    PcodeOp o6 = mkNoOut(Op::Return, {});
    o6.address = 0x3001;

    fn.ops = {o0, o1, o2, o3, o4, o5, o6};
    // Raw stream: Memory-space targets are rejected, so the strcpy (behind the
    // dispatch, past the unconditional Branch) is NOT reached.
    REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}

TEST_CASE("pcode-encoder: MBA select (a & c) | (b & ~c) is already the bitwise-select form",
          "[pcode][mba]") {
    // The bitwise-select is itself the canonical form for a general mask; no
    // simpler Z3 representation exists, so simplifyMba leaves it unchanged.
    z3::context ctx;
    z3::expr a = ctx.bv_const("a", 8);
    z3::expr b = ctx.bv_const("b", 8);
    z3::expr c = ctx.bv_const("c", 8);
    z3::expr e = (a & c) | (b & ~c);
    z3::expr s = fold::symbolic::simplifyMba(e);
    REQUIRE(z3::eq(s, e)); // structurally unchanged
}

TEST_CASE("pcode-encoder: MBA xor (x | y) - (x & y) reduces to x ^ y", "[pcode][mba]") {
    z3::context ctx;
    z3::expr x = ctx.bv_const("x", 8);
    z3::expr y = ctx.bv_const("y", 8);
    z3::expr e = (x | y) - (x & y);
    z3::expr s = fold::symbolic::simplifyMba(e);
    REQUIRE(s.is_app());
    REQUIRE(s.decl().decl_kind() == Z3_OP_BXOR);
    z3::solver sol(ctx);
    sol.add(s != e);
    REQUIRE(sol.check() == z3::unsat);
}

TEST_CASE("pcode-encoder: MBA and (x + y) - (x | y) reduces to x & y", "[pcode][mba]") {
    z3::context ctx;
    z3::expr x = ctx.bv_const("x", 8);
    z3::expr y = ctx.bv_const("y", 8);
    z3::expr e = (x + y) - (x | y);
    z3::expr s = fold::symbolic::simplifyMba(e);
    REQUIRE(s.is_app());
    REQUIRE(s.decl().decl_kind() == Z3_OP_BAND);
    z3::solver sol(ctx);
    sol.add(s != e);
    REQUIRE(sol.check() == z3::unsat);
}

TEST_CASE("pcode-encoder: MBA or (x + y) - (x & y) reduces to x | y", "[pcode][mba]") {
    z3::context ctx;
    z3::expr x = ctx.bv_const("x", 8);
    z3::expr y = ctx.bv_const("y", 8);
    z3::expr e = (x + y) - (x & y);
    z3::expr s = fold::symbolic::simplifyMba(e);
    REQUIRE(s.is_app());
    REQUIRE(s.decl().decl_kind() == Z3_OP_BOR);
    z3::solver sol(ctx);
    sol.add(s != e);
    REQUIRE(sol.check() == z3::unsat);
}

TEST_CASE("pcode-encoder: non-MBA expression is unchanged", "[pcode][mba]") {
    z3::context ctx;
    z3::expr x = ctx.bv_const("x", 8);
    z3::expr y = ctx.bv_const("y", 8);
    z3::expr e = (x & y) | (x ^ y); // not a known MBA identity
    z3::expr s = fold::symbolic::simplifyMba(e);
    REQUIRE(z3::eq(s, e)); // structurally unchanged
}