Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Figure out what to do about random_seed #2989

Open
konnov opened this issue Sep 18, 2024 · 0 comments
Open

Figure out what to do about random_seed #2989

konnov opened this issue Sep 18, 2024 · 0 comments
Labels
feature A new feature or functionality FSMT Feature: Improvements in the SMT encoding

Comments

@konnov
Copy link
Collaborator

konnov commented Sep 18, 2024

When we set z3.smt.logic = QF_LIA, Z3SolverContext fails on:

apalache/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

Line 64 in ce6028e

params.add("random_seed", config.randomSeed)

On one hand, we need a stable seed for reproducible experiments. On the other hand, it would be great to have the ability to restrict the logic.
@konnov konnov added FSMT Feature: Improvements in the SMT encoding feature A new feature or functionality labels Sep 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
feature A new feature or functionality FSMT Feature: Improvements in the SMT encoding
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@konnov