From 01cf9f3c30c0bff98d01422a09d5a4e0d64b09f7 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Tue, 28 Nov 2023 21:02:50 -0800 Subject: [PATCH 01/13] stp support --- rosette/solver/smt/stp.rkt | 68 ++++++++++++++++++++++++++++++++++++++ test/all-rosette-tests.rkt | 34 ++++++++++--------- 2 files changed, 87 insertions(+), 15 deletions(-) create mode 100644 rosette/solver/smt/stp.rkt diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt new file mode 100644 index 00000000..f98ac5ad --- /dev/null +++ b/rosette/solver/smt/stp.rkt @@ -0,0 +1,68 @@ +#lang racket + +(require racket/runtime-path + "server.rkt" "env.rkt" + "../solver.rkt" + (prefix-in base/ "base-solver.rkt")) + +(provide (rename-out [make-stp stp]) stp? stp-available?) + +(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp")) +(define stp-opts '()) + +(define (stp-available?) + (not (false? (base/find-solver "stp" stp-path #f)))) + +(define (make-stp [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f]) + (define config + (cond + [(stp? solver) + (base/solver-config solver)] + [else + (define real-stp-path (base/find-solver "stp" stp-path path)) + (when (and (false? real-stp-path) (not (getenv "PLT_PKG_BUILD_SERVICE"))) + (error 'stp "stp binary is not available (expected to be at ~a); try passing the #:path argument to (stp)" (path->string (simplify-path stp-path)))) + (base/config options real-stp-path logic)])) + (stp (server (base/config-path config) stp-opts (base/make-send-options config)) config '() '() '() (env) '())) + +(struct stp base/solver () + #:property prop:solver-constructor make-stp + #:methods gen:custom-write + [(define (write-proc self port mode) (fprintf port "#"))] + #:methods gen:solver + [ + (define (solver-features self) + '(qf_bv)) + + (define (solver-options self) + (base/solver-options self)) + + (define (solver-assert self bools) + (base/solver-assert self bools)) + + (define (solver-minimize self nums) + (base/solver-minimize self nums)) + + (define (solver-maximize self nums) + (base/solver-maximize self nums)) + + (define (solver-clear self) + (base/solver-clear self)) + + (define (solver-shutdown self) + (base/solver-shutdown self)) + + (define (solver-push self) + (base/solver-push self)) + + (define (solver-pop self [k 1]) + (base/solver-pop self k)) + + (define (solver-check self) + (base/solver-check self)) + + (define (solver-debug self) + (base/solver-debug self))]) + +(define (set-default-options server) + void) \ No newline at end of file diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index c0086f7b..73fe1397 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -6,6 +6,7 @@ rosette/solver/smt/boolector rosette/solver/smt/cvc5 rosette/solver/smt/bitwuzla + rosette/solver/smt/stp "config.rkt") (error-print-width default-error-print-width) @@ -76,21 +77,24 @@ (define (slow-tests) - (when (cvc4-available?) - (printf "===== Running CVC4 tests =====\n") - (run-tests-with-solver cvc4)) - - (when (boolector-available?) - (printf "===== Running Boolector tests =====\n") - (run-tests-with-solver boolector)) - - (when (cvc5-available?) - (printf "===== Running cvc5 tests =====\n") - (run-tests-with-solver cvc5)) - - (when (bitwuzla-available?) - (printf "===== Running bitwuzla tests =====\n") - (run-tests-with-solver bitwuzla)) + ; (when (cvc4-available?) + ; (printf "===== Running CVC4 tests =====\n") + ; (run-tests-with-solver cvc4)) + + ; (when (boolector-available?) + ; (printf "===== Running Boolector tests =====\n") + ; (run-tests-with-solver boolector)) + + ; (when (cvc5-available?) + ; (printf "===== Running cvc5 tests =====\n") + ; (run-tests-with-solver cvc5)) + + ; (when (bitwuzla-available?) + ; (printf "===== Running bitwuzla tests =====\n") + ; (run-tests-with-solver bitwuzla)) + (when (stp-available?) + (printf "===== Running stp tests =====\n") + (run-tests-with-solver stp)) ) (module+ test From cd7c0740b87332b8985ad4337ea337025e7dbd67 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Thu, 30 Nov 2023 15:28:30 -0800 Subject: [PATCH 02/13] added yices2 --- test/all-rosette-tests.rkt | 29 ++++++++++++++++------------- test/base/bitvector.rkt | 7 +++++-- 2 files changed, 21 insertions(+), 15 deletions(-) diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index 73fe1397..14cad2b2 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -7,8 +7,8 @@ rosette/solver/smt/cvc5 rosette/solver/smt/bitwuzla rosette/solver/smt/stp + rosette/solver/smt/yices-smt2 "config.rkt") - (error-print-width default-error-print-width) @@ -77,24 +77,27 @@ (define (slow-tests) - ; (when (cvc4-available?) - ; (printf "===== Running CVC4 tests =====\n") - ; (run-tests-with-solver cvc4)) + (when (cvc4-available?) + (printf "===== Running CVC4 tests =====\n") + (run-tests-with-solver cvc4)) - ; (when (boolector-available?) - ; (printf "===== Running Boolector tests =====\n") - ; (run-tests-with-solver boolector)) + (when (boolector-available?) + (printf "===== Running Boolector tests =====\n") + (run-tests-with-solver boolector)) - ; (when (cvc5-available?) - ; (printf "===== Running cvc5 tests =====\n") - ; (run-tests-with-solver cvc5)) + (when (cvc5-available?) + (printf "===== Running cvc5 tests =====\n") + (run-tests-with-solver cvc5)) - ; (when (bitwuzla-available?) - ; (printf "===== Running bitwuzla tests =====\n") - ; (run-tests-with-solver bitwuzla)) + (when (bitwuzla-available?) + (printf "===== Running bitwuzla tests =====\n") + (run-tests-with-solver bitwuzla)) (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)) ) (module+ test diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt index d8430091..f3d3d03e 100644 --- a/test/base/bitvector.rkt +++ b/test/base/bitvector.rkt @@ -1,12 +1,15 @@ #lang racket (require rackunit rackunit/text-ui racket/generator (rename-in rackunit [check-exn rackunit/check-exn]) - rosette/solver/solution + rosette/solver/solution + ; (only-in rosette solver-features current-solver) "solver.rkt" + ; rosette/solver/smt/yices-smt2 rosette/lib/roseunit rosette/solver/smt/boolector racket/fixnum rosette/base/core/term rosette/base/core/bool rosette/base/core/result + ; rosette/solver/smt/server (except-in rosette/base/core/bitvector bv) (only-in rosette/base/core/bitvector [bv @bv]) rosette/base/core/polymorphic rosette/base/core/merge @@ -26,7 +29,7 @@ (define maxval+1 (expt 2 (sub1 (bitvector-size BV)))) (define maxval (sub1 maxval+1)) (define (bv v [t BV]) (@bv v t)) - +; (output-smt "output-debug/") (define-syntax-rule (check-exn e ...) (begin (rackunit/check-exn e ...) From 5994ae286a584e3035be92e95dd14e0e1e81704d Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Tue, 5 Dec 2023 18:03:37 -0800 Subject: [PATCH 03/13] yices2 addition --- rosette/solver/smt/yices-smt2.rkt | 68 +++++++++++++++++++++++++++++++ test/base/bitvector.rkt | 4 -- 2 files changed, 68 insertions(+), 4 deletions(-) create mode 100644 rosette/solver/smt/yices-smt2.rkt diff --git a/rosette/solver/smt/yices-smt2.rkt b/rosette/solver/smt/yices-smt2.rkt new file mode 100644 index 00000000..484f5f0b --- /dev/null +++ b/rosette/solver/smt/yices-smt2.rkt @@ -0,0 +1,68 @@ +#lang racket + +(require racket/runtime-path + "server.rkt" "env.rkt" + "../solver.rkt" + (prefix-in base/ "base-solver.rkt")) + +(provide (rename-out [make-yices-smt2 yices-smt2]) yices-smt2? yices-smt2-available?) + +(define-runtime-path yices-smt2-path (build-path ".." ".." ".." "bin" "yices-smt2")) +(define yices-smt2-opts '("--incremental")) + +(define (yices-smt2-available?) + (not (false? (base/find-solver "yices-smt2" yices-smt2-path #f)))) +(define default-logic 'QF_BV) ;; YICES_2 needs a default logic set otherwise it will error +(define (make-yices-smt2 [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f]) + (define config + (cond + [(yices-smt2? solver) + (base/solver-config solver)] + [else + (define real-yices-smt2-path (base/find-solver "yices-smt2" yices-smt2-path path)) + (when (and (false? real-yices-smt2-path) (not (getenv "PLT_PKG_BUILD_SERVICE"))) + (error 'yices-smt2 "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices-smt2)" (path->string (simplify-path yices-smt2-path)))) + (base/config options real-yices-smt2-path logic)])) + (yices-smt2 (server (base/config-path config) yices-smt2-opts (base/make-send-options config)) config '() '() '() (env) '())) + +(struct yices-smt2 base/solver () + #:property prop:solver-constructor make-yices-smt2 + #:methods gen:custom-write + [(define (write-proc self port mode) (fprintf port "#"))] + #:methods gen:solver + [ + (define (solver-features self) + '(qf_bv)) + + (define (solver-options self) + (base/solver-options self)) + + (define (solver-assert self bools) + (base/solver-assert self bools)) + + (define (solver-minimize self nums) + (base/solver-minimize self nums)) + + (define (solver-maximize self nums) + (base/solver-maximize self nums)) + + (define (solver-clear self) + (base/solver-clear self)) + + (define (solver-shutdown self) + (base/solver-shutdown self)) + + (define (solver-push self) + (base/solver-push self)) + + (define (solver-pop self [k 1]) + (base/solver-pop self k)) + + (define (solver-check self) + (base/solver-check self)) + + (define (solver-debug self) + (base/solver-debug self))]) + +(define (set-default-options server) + void) \ No newline at end of file diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt index f3d3d03e..4a46d525 100644 --- a/test/base/bitvector.rkt +++ b/test/base/bitvector.rkt @@ -2,14 +2,11 @@ (require rackunit rackunit/text-ui racket/generator (rename-in rackunit [check-exn rackunit/check-exn]) rosette/solver/solution - ; (only-in rosette solver-features current-solver) "solver.rkt" - ; rosette/solver/smt/yices-smt2 rosette/lib/roseunit rosette/solver/smt/boolector racket/fixnum rosette/base/core/term rosette/base/core/bool rosette/base/core/result - ; rosette/solver/smt/server (except-in rosette/base/core/bitvector bv) (only-in rosette/base/core/bitvector [bv @bv]) rosette/base/core/polymorphic rosette/base/core/merge @@ -29,7 +26,6 @@ (define maxval+1 (expt 2 (sub1 (bitvector-size BV)))) (define maxval (sub1 maxval+1)) (define (bv v [t BV]) (@bv v t)) -; (output-smt "output-debug/") (define-syntax-rule (check-exn e ...) (begin (rackunit/check-exn e ...) From 82a345850e5e1c70b6d77abb9d4cc6939734aa3e Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:27:47 -0800 Subject: [PATCH 04/13] workflow --- .github/workflows/tests.yml | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 735b631d..54d0ddb5 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -29,6 +29,7 @@ jobs: - name: Install solvers run: | mkdir bin && + wget $CVC4_URL -nv -O bin/cvc4 && chmod +x bin/cvc4 && wget $BOOLECTOR_URL -nv -O boolector.tar.gz && @@ -57,7 +58,25 @@ jobs: ninja && popd && popd && - cp bitwuzla/build/src/main/bitwuzla bin/ + cp bitwuzla/build/src/main/bitwuzla bin/ && + + sudo apt-get install -y git cmake bison flex libboost-all-dev python2 perl && + git clone https://github.com/stp/stp && + pushd stp && + git submodule init && git submodule update && + ./scripts/deps/setup-gtest.sh && + ./scripts/deps/setup-outputcheck.sh && + ./scripts/deps/setup-cms.sh && + ./scripts/deps/setup-minisat.sh && + mkdir build && + cd build && + cmake .. && + cmake --build . && + cp stp bin/ && + add-apt-repository -y ppa:sri-csl/formal-methods && + apt-get update && + apt-get install -y yices2 + - name: Install Rosette run: raco pkg install --auto --name rosette - name: Compile Rosette tests From ad210a6a2582bcadad8705e52a0daa914e34ef80 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:28:53 -0800 Subject: [PATCH 05/13] add some sudos --- .github/workflows/tests.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 54d0ddb5..73da38f8 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -73,9 +73,9 @@ jobs: cmake .. && cmake --build . && cp stp bin/ && - add-apt-repository -y ppa:sri-csl/formal-methods && - apt-get update && - apt-get install -y yices2 + sudo add-apt-repository -y ppa:sri-csl/formal-methods && + sudo apt-get update && + sudo apt-get install -y yices2 - name: Install Rosette run: raco pkg install --auto --name rosette From 3e69e044bc09453e60f1520ce6445755cc8c9923 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:32:59 -0800 Subject: [PATCH 06/13] delete some random whitespace --- .github/workflows/tests.yml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 73da38f8..bd89e86f 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -29,7 +29,6 @@ jobs: - name: Install solvers run: | mkdir bin && - wget $CVC4_URL -nv -O bin/cvc4 && chmod +x bin/cvc4 && wget $BOOLECTOR_URL -nv -O boolector.tar.gz && @@ -59,7 +58,6 @@ jobs: popd && popd && cp bitwuzla/build/src/main/bitwuzla bin/ && - sudo apt-get install -y git cmake bison flex libboost-all-dev python2 perl && git clone https://github.com/stp/stp && pushd stp && @@ -76,7 +74,6 @@ jobs: sudo add-apt-repository -y ppa:sri-csl/formal-methods && sudo apt-get update && sudo apt-get install -y yices2 - - name: Install Rosette run: raco pkg install --auto --name rosette - name: Compile Rosette tests From 7aeac356185e55ac3f13c345fd6f6ca0ab8cf218 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:36:27 -0800 Subject: [PATCH 07/13] end files in newline --- rosette/solver/smt/stp.rkt | 3 ++- rosette/solver/smt/yices-smt2.rkt | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index f98ac5ad..3377561e 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -65,4 +65,5 @@ (base/solver-debug self))]) (define (set-default-options server) - void) \ No newline at end of file + void) + \ No newline at end of file diff --git a/rosette/solver/smt/yices-smt2.rkt b/rosette/solver/smt/yices-smt2.rkt index 484f5f0b..d5be70c0 100644 --- a/rosette/solver/smt/yices-smt2.rkt +++ b/rosette/solver/smt/yices-smt2.rkt @@ -65,4 +65,5 @@ (base/solver-debug self))]) (define (set-default-options server) - void) \ No newline at end of file + void) + \ No newline at end of file From 507a9a74b600053b236e0d0b36e16ee8eeadc8b5 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:45:01 -0800 Subject: [PATCH 08/13] fix added whitespace --- test/base/bitvector.rkt | 1 + 1 file changed, 1 insertion(+) diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt index 4a46d525..07331c61 100644 --- a/test/base/bitvector.rkt +++ b/test/base/bitvector.rkt @@ -26,6 +26,7 @@ (define maxval+1 (expt 2 (sub1 (bitvector-size BV)))) (define maxval (sub1 maxval+1)) (define (bv v [t BV]) (@bv v t)) + (define-syntax-rule (check-exn e ...) (begin (rackunit/check-exn e ...) From 1c531f351d2e02fae79aab07b64a18f9dc9e61f2 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 19:23:04 -0800 Subject: [PATCH 09/13] fix workflows test --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index bd89e86f..37e28397 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -70,7 +70,7 @@ jobs: cd build && cmake .. && cmake --build . && - cp stp bin/ && + cp stp bin/stp && sudo add-apt-repository -y ppa:sri-csl/formal-methods && sudo apt-get update && sudo apt-get install -y yices2 From 47450f07648c2183d097c7074c37cf7b4d1dc0b5 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 19:30:11 -0800 Subject: [PATCH 10/13] fix path --- .github/workflows/tests.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 37e28397..0c411152 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -70,6 +70,8 @@ jobs: cd build && cmake .. && cmake --build . && + popd && + popd && cp stp bin/stp && sudo add-apt-repository -y ppa:sri-csl/formal-methods && sudo apt-get update && From eab000174aa8df904fe388cf2fb0674f61d0cd10 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 19:30:31 -0800 Subject: [PATCH 11/13] bin should be in right folder now --- .github/workflows/tests.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 0c411152..5656ea27 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -67,12 +67,12 @@ jobs: ./scripts/deps/setup-cms.sh && ./scripts/deps/setup-minisat.sh && mkdir build && - cd build && + pushd build && cmake .. && cmake --build . && popd && popd && - cp stp bin/stp && + cp stp/build/stp bin/stp && sudo add-apt-repository -y ppa:sri-csl/formal-methods && sudo apt-get update && sudo apt-get install -y yices2 From 53fd00a5c5387d06052e1707406b75fcff4932be Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Thu, 7 Dec 2023 11:59:15 -0800 Subject: [PATCH 12/13] debugging for stp failure --- test/all-rosette-tests.rkt | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index 14cad2b2..5ae1aefb 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -77,21 +77,21 @@ (define (slow-tests) - (when (cvc4-available?) - (printf "===== Running CVC4 tests =====\n") - (run-tests-with-solver cvc4)) + ; (when (cvc4-available?) + ; (printf "===== Running CVC4 tests =====\n") + ; (run-tests-with-solver cvc4)) - (when (boolector-available?) - (printf "===== Running Boolector tests =====\n") - (run-tests-with-solver boolector)) + ; (when (boolector-available?) + ; (printf "===== Running Boolector tests =====\n") + ; (run-tests-with-solver boolector)) - (when (cvc5-available?) - (printf "===== Running cvc5 tests =====\n") - (run-tests-with-solver cvc5)) + ; (when (cvc5-available?) + ; (printf "===== Running cvc5 tests =====\n") + ; (run-tests-with-solver cvc5)) - (when (bitwuzla-available?) - (printf "===== Running bitwuzla tests =====\n") - (run-tests-with-solver bitwuzla)) + ; (when (bitwuzla-available?) + ; (printf "===== Running bitwuzla tests =====\n") + ; (run-tests-with-solver bitwuzla)) (when (stp-available?) (printf "===== Running stp tests =====\n") (run-tests-with-solver stp)) @@ -101,5 +101,6 @@ ) (module+ test - (fast-tests) - (slow-tests)) + ; (fast-tests) + (slow-tests) + ) From 3f01d861b97bec7e018a95191497f70efaebf0ef Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Thu, 7 Dec 2023 14:02:13 -0800 Subject: [PATCH 13/13] some debugging info and output --- rosette/solver/smt/stp.rkt | 2 +- test/all-rosette-tests.rkt | 70 +++++++++++++++++++------------------- test/base/push-pop.rkt | 2 +- 3 files changed, 37 insertions(+), 37 deletions(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index 3377561e..59c54e1e 100644 --- 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 index 5ae1aefb..c95d3257 100644 --- 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 index 30d201e9..3d33e4df 100644 --- 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)))