Cut down the features to just BV

emina · Sep 11, 2023 · 3380a00 · 3380a00
1 parent 4851d5d
commit 3380a00
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/rosette/solver/smt/bitwuzla.rkt b/rosette/solver/smt/bitwuzla.rkt
@@ -39,7 +39,7 @@
   #:methods gen:solver
   [
    (define (solver-features self)
-     '(qf_bv qf_uf))
+     '(qf_bv))
 
    (define (solver-options self)
      (base/solver-options self))

diff --git a/rosette/solver/smt/cvc5.rkt b/rosette/solver/smt/cvc5.rkt
@@ -32,7 +32,7 @@
   #:methods gen:solver
   [
    (define (solver-features self)
-     '(qf_bv qf_uf qf_lia qf_nia qf_lra qf_nra quantifiers int2bv))
+     '(qf_bv))
 
    (define (solver-options self)
      (base/solver-options self))