mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 21:16:02 +00:00
Code Activity

add bash files for test runs

Browse source
This commit is contained in:
Ilana Shapiro 2025-07-25 15:34:26 -07:00
parent 4b87458ce2
commit 65504953f7
2 changed files with 32 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

31
run_local_tests.sh Executable file
View file

@ -0,0 +1,31 @@
#!/bin/bash
# run from inside ./z3/build
Z3=./z3
OPTIONS="-v:0 -st smt.threads=4"
OUT_FILE="../z3_results.txt"
BASE_PATH="../../z3-poly-testing/inputs/"
# List of relative test files (relative to BASE_PATH)
REL_TEST_FILES=(
"QF_NIA_small/Ton_Chanh_15__Singapore_v1_false-termination.c__p27381_terminationG_0.smt2"
"QF_UFDTLIA_SAT/52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2"
)
# Clear output file
> "$OUT_FILE"
# Loop through and run Z3 on each file
for rel_path in "${REL_TEST_FILES[@]}"; do
full_path="$BASE_PATH$rel_path"
test_name="$rel_path"
echo "Running: $test_name"
echo "===== $test_name =====" >> "$OUT_FILE"
$Z3 "$full_path" $OPTIONS >> "$OUT_FILE" 2>&1
echo "" >> "$OUT_FILE"
done
echo "Results written to $OUT_FILE"

2
src/smt/smt_context.h
View file

@ -189,7 +189,7 @@ namespace smt {
unsigned_vector m_lit_occs; //!< occurrence count of literals
svector<bool_var_data> m_bdata; //!< mapping bool_var -> data
svector<double> m_activity;
svector<double[2]> m_scores;
svector<std::array<double, 2>> m_scores;
clause_vector m_aux_clauses;
clause_vector m_lemmas;
vector<clause_vector> m_clauses_to_reinit;