some debugging info and output

vcanumalla · Dec 7, 2023 · 3f01d86 · 3f01d86
1 parent 53fd00a
commit 3f01d86
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 37 deletions.
diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt
@@ -8,7 +8,7 @@
 (provide (rename-out [make-stp stp]) stp? stp-available?)
 
 (define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
-(define stp-opts '())
+(define stp-opts '("--SMTLIB2" "-p"))
 
 (define (stp-available?)
   (not (false? (base/find-solver "stp" stp-path #f))))

diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt
@@ -20,39 +20,39 @@
 
 
 (require-all-tests
- "base/type.rkt"
- "base/term.rkt"
- "base/bool.rkt"
- "base/merge.rkt"
- "base/store.rkt"
- "base/vc.rkt"
- "base/eval-guarded.rkt"
- "base/list.rkt"
- "base/vector.rkt"
- "base/bvseq.rkt"
- "base/forall.rkt"
- "base/bitvector.rkt"
- "base/bvlib.rkt"
- "base/equality.rkt"
- "base/uninterpreted.rkt"
- "base/real.rkt"
- "base/quantified.rkt"
- "base/finitize.rkt"
- "base/distinct.rkt"
- "base/generics.rkt"
+;  "base/type.rkt"
+;  "base/term.rkt"
+;  "base/bool.rkt"
+;  "base/merge.rkt"
+;  "base/store.rkt"
+;  "base/vc.rkt"
+;  "base/eval-guarded.rkt"
+;  "base/list.rkt"
+;  "base/vector.rkt"
+;  "base/bvseq.rkt"
+;  "base/forall.rkt"
+;  "base/bitvector.rkt"
+;  "base/bvlib.rkt"
+;  "base/equality.rkt"
+;  "base/uninterpreted.rkt"
+;  "base/real.rkt"
+;  "base/quantified.rkt"
+;  "base/finitize.rkt"
+;  "base/distinct.rkt"
+;  "base/generics.rkt"
  "base/push-pop.rkt"
- "base/optimize-order.rkt"
- "base/reflect.rkt"
- "base/decode.rkt"
- "query/solve.rkt"
- "query/verify.rkt"
- "query/synthesize.rkt"
- "query/solve+.rkt"
- "query/synthax.rkt"
- "query/grammar.rkt"
- "query/optimize.rkt"
- "lib/destruct.rkt"
- "profile/test.rkt"
+;  "base/optimize-order.rkt"
+;  "base/reflect.rkt"
+;  "base/decode.rkt"
+;  "query/solve.rkt"
+;  "query/verify.rkt"
+;  "query/synthesize.rkt"
+;  "query/solve+.rkt"
+;  "query/synthax.rkt"
+;  "query/grammar.rkt"
+;  "query/optimize.rkt"
+;  "lib/destruct.rkt"
+;  "profile/test.rkt"
  "trace/test.rkt")
 
 
@@ -95,9 +95,9 @@
   (when (stp-available?)
     (printf "===== Running stp tests =====\n")
     (run-tests-with-solver stp))
-  (when (yices-smt2-available?)
-    (printf "===== Running yices-smt2 tests =====\n")
-    (run-tests-with-solver yices-smt2))
+  ; (when (yices-smt2-available?)
+  ;   (printf "===== Running yices-smt2 tests =====\n")
+  ;   (run-tests-with-solver yices-smt2))
 )
 
 (module+ test

diff --git a/test/base/push-pop.rkt b/test/base/push-pop.rkt
@@ -14,7 +14,7 @@
 (define push-pop-tests
   (test-suite+ "Tests for the push / pop interface."
    #:features '(qf_bv)
-         
+  (output-smt "push-pop-tests.smt2")
   (define solver (current-solver))
   (check-exn exn:fail? (thunk (solver-pop solver)))