View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
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 | ||||||
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' | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
rwmjones (reporter) 2020-10-15 10:08 |
I filed this in gitlab: https://git.frama-c.com/pub/frama-c/-/issues/33 |
correnson (manager) 2020-10-15 10:58 |
Duplicate with pub/frama-c#33 |
![]() |
|||
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 |