Frama-C Bug Tracking System - Frama-C |
| View Issue Details |
|
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002509 | Frama-C | Plug-in > wp | public | 2020-10-15 10:06 | 2020-10-15 10:58 |
|
| Reporter | rwmjones | |
| Assigned To | correnson | |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Status | closed | Resolution | duplicate | |
| Platform | | OS | | OS Version | |
| Product Version | | |
| Target Version | | Fixed in Version | | |
|
| Summary | 0002509: z3 ERROR: unknown parameter 'model_compress' |
| Description | Apparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258 |
| Steps To Reproduce | Use z3 4.8.9, turn on debugging.
<6.827036,call_prover>Call_provers: actual command is:
z3 -smt2 -t:10000 sat.random_seed=42
model_compress=false nlsat.randomize=false
smt.random_seed=42 -st
/tmp/why_b9efc2_zilch-T-wp_goal.smt2
ERROR: unknown parameter 'model_compress'
|
| Additional Information | |
| Tags | No tags attached. |
| Relationships | |
| Attached Files | |
|
| Issue History |
| Date Modified | Username | Field | Change |
| 2020-10-15 10:06 | rwmjones | New Issue | |
| 2020-10-15 10:06 | rwmjones | Status | new => assigned |
| 2020-10-15 10:06 | rwmjones | Assigned To | => correnson |
| 2020-10-15 10:08 | rwmjones | Note Added: 0006981 | |
| 2020-10-15 10:58 | correnson | Note Added: 0006982 | |
| 2020-10-15 10:58 | correnson | Status | assigned => closed |
| 2020-10-15 10:58 | correnson | Resolution | open => duplicate |