Closed felixonmars closed 2 years ago
Here are some test failure examples.
memory_high_watermark_mb
IMHO the test suite should not rely on these details.
Basics.QueryIndividual query_badOption: FAIL (5.02s) --- SBVTestSuite/GoldFiles/query_badOption.gold 2022-10-16 00:20:34.000000000 +0200 +++ SBVTestSuite/GoldFiles/query_badOption.gold_temp 2022-10-16 00:38:51.730627132 +0200 @@ -19,6 +19,7 @@ *** dump_models (bool) (default: false) *** encoding (string) (default: unicode) *** memory_high_watermark (unsigned int) (default: 0) +*** memory_high_watermark_mb (unsigned int) (default: 0) *** memory_max_alloc_count (unsigned int) (default: 0) *** memory_max_size (unsigned int) (default: 0) *** model (bool) (default: true) @@ -37,7 +38,7 @@ *** well_sorted_check (bool) (default: false)") *** *** Exit code : ExitFailure (-15) -*** Executable: /usr/local/bin/z3 +*** Executable: /usr/bin/z3 *** Options : -nw -in -smt2 *** *** Reason : Backend solver reports it does not support this option. Use -p '/query_badOption/' to rerun this test only. Basics.Query query1: FAIL (0.05s) --- SBVTestSuite/GoldFiles/query1.gold 2022-10-16 00:20:34.000000000 +0200 +++ SBVTestSuite/GoldFiles/query1.gold_temp 2022-10-16 00:38:52.153962377 +0200 @@ -79,7 +79,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version) -[RECV] (:version "4.8.17") +[RECV] (:version "4.11.2") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -110,7 +110,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.8.17") +[RECV] (:version "4.11.2") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) Use -p '/query1/' to rerun this test only.
I don't expect other people to run the test-suite; it's mostly for internal development purposes only. (And hard to modify gold-files post-facto to accommodate paths/version etc.)
I see. Thanks for the info.
Here are some test failure examples.
memory_high_watermark_mb
comes from a full "Legal parameters" list from z3's output and should not matter.IMHO the test suite should not rely on these details.