{"record":{"id":"4b966b9495a78658","repo":"diem/diem","slug":"internal-boogie-exited-with-compilation-errors","errorCode":null,"errorMessage":"[internal] boogie exited with compilation errors:\n{}","messagePattern":"\\[internal\\] boogie exited with compilation errors:\n(.+?)","errorType":"exception","errorClass":null,"httpStatus":null,"severity":"error","filePath":"language/move-prover/boogie-backend/src/boogie_wrapper.rs","lineNumber":192,"sourceCode":"                }\n            ));\n        }\n        if !output.status.success() {\n            // Exit here with raw output.\n            return Err(anyhow!(\n                \"Boogie error ({}): {}\\n\\nstderr:\\n{}\",\n                output.status,\n                out,\n                err\n            ));\n        }\n        if out.trim().starts_with(\"Unable to monomorphize\") {\n            return Err(anyhow!(\"Boogie error: {}\\n\\nstderr:\\n{}\", out, err));\n        }\n        // Boogie output contains the string \"errors detected in\" whenever parsing,\n        // resolution, or type checking errors are discovered.\n        if out.contains(\"errors detected in\") {\n            return Err(anyhow!(\n                \"[internal] boogie exited with compilation errors:\\n{}\",\n                out\n            ));\n        }\n        if out.contains(\"Prover error:\") {\n            return Err(anyhow!(\n                \"[internal] boogie exited with prover errors:\\n{}\",\n                out\n            ));\n        }\n        let mut errors = self.extract_verification_errors(&out);\n        errors.extend(self.extract_inconclusive_errors(&out));\n        errors.extend(self.extract_inconsistency_errors(&out));\n        Ok(BoogieOutput {\n            errors,\n            all_output: out,\n        })\n    }","sourceCodeStart":174,"sourceCodeEnd":210,"githubUrl":"https://github.com/diem/diem/blob/fc4714a8ea273b6efe8b13dbce72ea60aad9a16c/language/move-prover/boogie-backend/src/boogie_wrapper.rs#L174-L210","documentation":"When Boogie's output contains \"errors detected in\", Boogie found parsing, resolution, or type-checking errors in the generated Boogie program. Because the generated program is produced by the Move-to-Boogie translator, this is labeled [internal]: it indicates a translator/Boogie interface problem rather than a user verification failure. The raw Boogie output is included for diagnosis.","triggerScenarios":"call_boogie when out.contains(\"errors detected in\") — i.e. the translated .bpl file failed Boogie's parse/resolution/type-check stage.","commonSituations":"Translator bugs on unusual Move constructs; Boogie version drift introducing new checks; corrupted .bpl temp files; verifying code generated by a different (older) move-prover translator.","solutions":["File/inspect issues against the move-to-boogie translator, since the .bpl input is generated — this is rarely a user code fix","Check the embedded Boogie output for the exact line/column of the resolution error","Confirm the installed Boogie version matches the expected one (versions are pinned in options.rs)","Re-run after `cargo clean` to rule out a stale translator binary mixing versions"],"exampleFix":null,"handlingStrategy":"try-catch","validationCode":null,"typeGuard":null,"tryCatchPattern":"match call_boogie(...) {\n    Err(e) if e.to_string().contains(\"[internal] boogie exited with compilation errors\") => {\n        // This indicates a translator bug or version mismatch, not user code.\n        eprintln!(\"{}\", e); // embedded output names the failing .bpl line\n        // report to move-prover maintainers\n    }\n    other => other,\n}","preventionTips":["Keep translator (move-prover) and Boogie versions aligned","Avoid untested/edge-case Move constructs in verified code until supported","Regenerate .bpl fresh (cargo clean) to rule out stale translator output","Check existing move-prover issues for known translator bugs before debugging"],"tags":["internal","boogie","translator","smt-solver"],"backgroundTag":"boogie-compilation-error","analyzedSha":"fc4714a8ea273b6efe8b13dbce72ea60aad9a16c","analyzedAt":"2026-09-04T21:07:05.890Z","contentChangedAt":"2026-09-04T21:07:05.890Z","schemaVersion":2},"datasetVersion":"2026-09-12T02:17:10.037Z"}