Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002509Frama-CPlug-in > wppublic2020-10-15 10:062020-10-15 10:58
Reporterrwmjones 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionduplicate 
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: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258
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 /tmp/why_b9efc2_zilch-T-wp_goal.smt2 ERROR: unknown parameter 'model_compress'
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006981)
rwmjones (reporter)
2020-10-15 10:08

I filed this in gitlab: https://git.frama-c.com/pub/frama-c/-/issues/33
(0006982)
correnson (manager)
2020-10-15 10:58

Duplicate with pub/frama-c#33

- 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


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker