Gaurav Parthasarathy (Nov 29 2023 at 19:07): Gaurav Parthasarathy (Nov 29 2023 at 19:07):Hi. On Windows, I run into the following scenario: I open theory files via the Isabelle GUI (jEdit) and then some smt tactics fail sometimes (not always the same ones). If I then rerun the tactic (e.g., by removing and adding the same smt tactic again), then the tactic usually succeeds. Whenever, I run the session via the Isabelle command line on Linux (Windows Subsystem), then I never get any errors. Has anyone run into this issue or knows how to resolve it?
Mathias Fleury (Nov 30 2023 at 08:36):This feels like some thread contention (Isabelle launching too many threads, so not much seems to happen)
Gaurav Parthasarathy (Dec 07 2023 at 08:45):Thanks for the answer! When I use declare [[smt_trace=true]] I seem to get a standard error message showing the SMT query that veriT uses (I have attached the error message). Is such a standard error message consistent with the view that the cause is thread contention? Could it be that the SMT solver is being invoked with different settings on different runs (for example, different random seeds)?
20230712_smt_tactic_failure_trace.txt
Last updated: Apr 27 2024 at 16:16 UTC