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.

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

Bitwuzla flag to make Xilinx not timeout #329

Closed
sorawee opened this issue Aug 7, 2023 · 1 comment
Closed

Bitwuzla flag to make Xilinx not timeout #329

sorawee opened this issue Aug 7, 2023 · 1 comment

Comments

@sorawee
Copy link
Collaborator

sorawee commented Aug 7, 2023

diff --git a/rosette/solver/smt/bitwuzla.rkt b/rosette/solver/smt/bitwuzla.rkt
index d5026c8..4b0a725 100644
--- a/rosette/solver/smt/bitwuzla.rkt
+++ b/rosette/solver/smt/bitwuzla.rkt
@@ -16,7 +16,7 @@
 (provide (rename-out [make-bitwuzla bitwuzla]) bitwuzla? bitwuzla-available?)

 (define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "bitwuzla"))
-(define bitwuzla-opts '("-m" "-i"))
+(define bitwuzla-opts '("-m" "--pp-elim-extracts"))

 (define (bitwuzla-available?)
   (not (false? (base/find-solver "bitwuzla" bitwuzla-path #f))))

I eliminated -i, since this option is not supported in my Bitwuzla. It's unclear how it has been working for you...

gussmith23 added a commit to gussmith23/rosette that referenced this issue Aug 7, 2023
See gussmith23/lakeroad#329

Co-authored-by: Sorawee Porncharoenwase <sorawee.pwase@gmail.com>
@gussmith23
Copy link
Owner

Added in emina/rosette#260

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants