0002509: z3 ERROR: unknown parameter 'model_compress'

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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'

Tags

No 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