Frama-C Bug Tracking System - Frama-C
View Issue Details
0002509Frama-CPlug-in > wppublic2020-10-15 10:062020-10-15 10:58
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002509: z3 ERROR: unknown parameter 'model_compress'
DescriptionApparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility:
Steps To ReproduceUse 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

ERROR: unknown parameter 'model_compress'
TagsNo tags attached.
Attached Files

2020-10-15 10:08   
I filed this in gitlab:
2020-10-15 10:58   
Duplicate with pub/frama-c#33

Issue History
2020-10-15 10:06rwmjonesNew Issue
2020-10-15 10:06rwmjonesStatusnew => assigned
2020-10-15 10:06rwmjonesAssigned To => correnson
2020-10-15 10:08rwmjonesNote Added: 0006981
2020-10-15 10:58corrensonNote Added: 0006982
2020-10-15 10:58corrensonStatusassigned => closed
2020-10-15 10:58corrensonResolutionopen => duplicate