recovered regr_smlp/data/smlp_toy_num_resp_noknobs.csv and regr_smlp/specs/smlp_toy_num_resp_noknobs_verify.spec by zurabksmlp · Pull Request #151 · SMLP-Systems/smlp

zurabksmlp · 2026-05-31T10:46:21Z

Recovered missing data and spec files for the "noknobs" tests:
57,61,62,65,66,67,68,71,72,73,74,75,76,78,84,139,144,162,163,184,185,186
All tests use the same data and spec files:
data:
regr_smlp/data/smlp_toy_num_resp_noknobs
specL
regr_smlp/specs/smlp_toy_num_resp_noknobs_verify.spec

These data and spec files are obtained simply by renaming variables: : x --> x0, p1 --> x1, p2 --> x3 irrespectively n:
regr_smlp/data/smlp_toy_num_resp_mult.csv
regr_smlp/specs/smlp_toy_num_resp_mult_verify.spec

I have checked these changes on Test57 and have a good confidence that the recovered files are as intended.
This addresses part of missing input files issue #147

…specs/smlp_toy_num_resp_noknobs_verify.spec

mdmitry1

There are many tests failed due to missing data:

echo n | env CUDA_VISIBLE_DEVICES=-1 python3.11 ./smlp_regr.py -t all -w 8 -def n -g |& tee noknobs_tests_recovery.smlp_regr.log
grep Failed noknobs_tests_recovery.smlp_regr.log

Test 73 Failed:
Test 74 Failed:
Test 75 Failed:
Test 139 Failed:
Test 162 Failed:
Test 163 Failed:
Test 184 Failed:
Test 185 Failed:
Test 186 Failed:

Master is not updated

2.1 Missing files in master

grep "File master" noknobs_tests_recovery.smlp_regr.log | awk '{print $3}' | cut -d_ -f1 | sort -u

Test144
Test57
Test61
Test62
test65
Test65
Test66
test67
Test67
Test68
test71
Test71
Test72
test76
Test76
test78
Test78
Test84

2.2 Diff(s) due smlp package structure change.

For example:

cat test76_model_smlp_model_term.json | tr ' ' '\012' | sort > test76_model_smlp_model_term_sorted.json
cat ../master/test76_model_smlp_model_term.json | tr ' ' '\012' | sort > test76_model_smlp_model_term_sorted_master.json
diff test76_model_smlp_model_term_sorted*.json

215,216c215,216
< <smlp.core.libsmlp.term2
< <smlp.core.libsmlp.term2
---
> <smlp.libsmlp.term2
> <smlp.libsmlp.term2

My results: code.tar.gz

Version validated:

pip show smlptech | grep Version

Version: 1.2.0

…57 and Test61

fbrausse · 2026-06-01T07:01:18Z

Checking this on my pytest branch we go from

= 31 failed, 163 passed, 38 skipped, 2 xfailed, 41 warnings in 558.42s (0:09:18) =

to

= 30 failed, 174 passed, 28 skipped, 2 xfailed, 32 warnings in 524.69s (0:08:44) =

Warnings removed concern path ../data/smlp_toy_num_resp_noknobs.csv (as expected for this PR), while new warnings are about:

-new_dat ../data/smlp_toy_num_resp_noknobs_pred_labeled.csv not existing (tests 73, 139, 162, 163, 184, 185, 186), and
-save_model t specified in args but no -model_name given (test 84).

…l files

mdmitry1 · 2026-06-01T10:03:39Z

Results after 0459981 checkin.
Regression command:

cd $(git rev-parse --show-toplevel)/tests/smlp_regression
./run_smlp_regression

All inputs are in place

grep -c Failed run_smlp_regression.log

Missing outputs run_smlp_regression.log

grep "File master" run_smlp_regression.log | awk '{print $3}' | cut -d_ -f1 | sort -u

Test139
Test144
Test162
Test163
Test184
Test185
Test186
Test61
Test62
Test65
test67
Test67
Test68
test71
Test71
Test72
test73
Test73
Test74
Test75
test76
Test76
test78
Test78
Test84

Diffs: run_smlp_regression_diff_report.log
All results: noknobs_tests_recovery_code.tar.gz

… models

fbrausse · 2026-06-01T12:26:07Z

Now even better:

= 33 failed, 180 passed, 19 skipped, 2 xfailed, 23 warnings in 546.12s (0:09:06) =

The 3 tests now failing that are new in wrt. before are 57, 65 and 66, due to

Details

Test57:

--- ../master/Test57_smlp_toy_num_resp_noknobs_verify_results.json	2026-06-01 14:02:21.048730624 +0200
+++ /tmp/pytest-of-kane/pytest-9/popen-gw13/test3/Test57_smlp_toy_num_resp_noknobs_verify_results.json	2026-06-01 14:03:44.418788290 +0200
@@ -4,10 +4,10 @@
 		"assertion_status": "FAIL",
 		"counter_example": {
 			"x0": 0.0,
-			"x1": 1.0,
+			"x1": 4.0,
 			"y1": 9.0,
-			"x2": 7.0,
-			"y2": 5.0
+			"x2": 6.000000067055225,
+			"y2": 9.0
 		},
 		"assertion_feasible": false
 	},

Test65

--- ../master/Test65_smlp_toy_num_resp_noknobs_verify_results.json	2026-06-01 14:02:21.054730700 +0200
+++ /tmp/pytest-of-kane/pytest-9/popen-gw6/test3/Test65_smlp_toy_num_resp_noknobs_verify_results.json	2026-06-01 14:03:49.898857820 +0200
@@ -10,7 +10,7 @@
 		"assertion_status": "FAIL",
 		"counter_example": {
 			"x0": 0.0,
-			"x1": 7.0,
+			"x1": 4.0,
 			"y1": 9.0,
 			"x2": 6.000000067055225,
 			"y2": 9.0

Test66

--- ../master/Test66_test65_model_trace.csv	2026-06-01 14:02:21.054730700 +0200
+++ /tmp/pytest-of-kane/pytest-9/popen-gw6/test4/Test66_test65_model_trace.csv	2026-06-01 14:04:04.129038377 +0200
@@ -1,9 +1,9 @@
 stage,solver,x0,x1,x2,y1,y2
 interface_consistency,sat,0,7,3
-model_consistency,sat,0,1,805306377/134217728,5,5
-witness_consistency,sat,0,1,805306377/134217728,5,5
-witness_consistency,sat,0,1,805306377/134217728,5,5
-ca,sat,0,1,6,5,5
+model_consistency,sat,0,7,805306377/134217728,9,9
+witness_consistency,sat,0,7,805306377/134217728,9,9
+witness_consistency,sat,0,7,805306377/134217728,9,9
+ca,sat,1,1,27/4,9,5
 ce,unsat
-ca,sat,0,7,671088649/134217728,5,9
-ce,sat,0,7,805306377/134217728,9,9
+ca,sat,0,1,1140850697/201326592,5,5
+ce,sat,0,4,805306377/134217728,9,9
--- ../master/Test66_test65_model_verify_results.json	2026-06-01 14:02:21.054730700 +0200
+++ /tmp/pytest-of-kane/pytest-9/popen-gw6/test4/Test66_test65_model_verify_results.json	2026-06-01 14:04:04.133038427 +0200
@@ -10,7 +10,7 @@
 		"assertion_status": "FAIL",
 		"counter_example": {
 			"x0": 0.0,
-			"x1": 7.0,
+			"x1": 4.0,
 			"y1": 9.0,
 			"x2": 6.000000067055225,
 			"y2": 9.0

…d models

…del files

…asters and models

mdmitry1 · 2026-06-01T19:46:23Z

Reproduced @fbrausse results for Test57:

diff Test57_smlp_toy_num_resp_noknobs_verify_results.json ../master/

7c7
< 			"x1": 4.0,
---
> 			"x1": 1.0,
9,10c9,10
< 			"x2": 6.000000067055225,
< 			"y2": 9.0
---
> 			"x2": 7.0,
> 			"y2": 5.0

mdmitry1 · 2026-06-02T06:18:43Z

Results after commit `88cdb5f` Mon Jun 1 23:19:50 2026 +0300

code.88cdb5f.tar.gz

All inputs are in place

grep -c Failed noknobs_tests_recovery.diff_report.log

Missing master files

grep "File master" noknobs_tests_recovery.smlp_regr.log | awk '{print $3}' | cut -d_ -f1 | sort -u

Test61
Test62
Test71

Diffs

$(git rev-parse --show-toplevel)/tests/smlp_regression/create_diff_report | grep Diff | awk '{print $5}' | awk -F_ '{print $1}' | tr -d Test | sort -un | nl

Results match exactly on two machines

Ubuntu 24.04
Windows 11/WSL2 with Ubuntu 24.04

SMLP packages

smlp_packages.txt

smlp_dependencies_tree.txt

fbrausse · 2026-06-02T08:40:55Z

Filtering out one more expected-to-fail test (229) as well as the three tests 145, 146 and 205 (for the reason mentioned in #149), pytest now arrives at

= 43 failed, 166 passed, 22 skipped, 3 xfailed, 26 warnings in 543.53s (0:09:03) =

mdmitry1

Fixed all diffs

recovered regr_smlp/data/smlp_toy_num_resp_noknobs.csv and regr_smlp/…

0d344b8

…specs/smlp_toy_num_resp_noknobs_verify.spec

zurabksmlp requested a review from mdmitry1 May 31, 2026 10:46

mdmitry1 requested changes May 31, 2026

View reviewed changes

added smlp_toy_num_resp_noknobs_pred_labeled.csv and masters for Test…

756f258

…57 and Test61

zurabksmlp added 2 commits June 1, 2026 10:12

updated master files for test 62

fbba95c

added Test65 and Test66 master files and test65_model master and mode…

0459981

…l files

added master for tests 67 and 68 and test67_model files in master and…

47736de

… models

zurabksmlp added 8 commits June 1, 2026 15:26

added masters for test 71 and 72 and test71_model files to masters an…

489bb61

…d models

added masters for test 61 and test 65 trace file

1e8d5de

added masters for test 73 and 74 and masters and models for test73_mo…

7e6e4c4

…del files

added test 75 masters

4224233

added masters for tests 76 and 77 and some of test76_model files to m…

172b2d6

…asters and models

added masters for tests 78 and 84

16bd143

added masters for tests 139 and 144

5854561

added masters for tests 162 and 163

2e752cb

added masters for tests 184,185,186

88cdb5f

mdmitry1 added 6 commits June 2, 2026 16:58

Fixed and added missing files in new tests

35129d1

Fixing issue in the previous checkin

8e5af0a

Changing one more file - side effect of Test76 change

ad0c15e

Adding file, missed in the previous commit

75057b4

Updated expected results for Docker

9fcf4b4

Updated expected results for virtual environment

45ac152

mdmitry1 approved these changes Jun 2, 2026

View reviewed changes

mdmitry1 requested a review from fbrausse June 2, 2026 17:17

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

recovered regr_smlp/data/smlp_toy_num_resp_noknobs.csv and regr_smlp/specs/smlp_toy_num_resp_noknobs_verify.spec#151

recovered regr_smlp/data/smlp_toy_num_resp_noknobs.csv and regr_smlp/specs/smlp_toy_num_resp_noknobs_verify.spec#151
zurabksmlp wants to merge 20 commits into
masterfrom
noknobs_tests_recovery

zurabksmlp commented May 31, 2026

Uh oh!

mdmitry1 left a comment

Uh oh!

fbrausse commented Jun 1, 2026

Uh oh!

mdmitry1 commented Jun 1, 2026

Uh oh!

fbrausse commented Jun 1, 2026

Uh oh!

mdmitry1 commented Jun 1, 2026

Uh oh!

mdmitry1 commented Jun 2, 2026 •

edited

Loading

Uh oh!

fbrausse commented Jun 2, 2026

Uh oh!

mdmitry1 left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

zurabksmlp commented May 31, 2026

Uh oh!

mdmitry1 left a comment

Choose a reason for hiding this comment

Uh oh!

fbrausse commented Jun 1, 2026

Uh oh!

mdmitry1 commented Jun 1, 2026

Uh oh!

fbrausse commented Jun 1, 2026

Uh oh!

mdmitry1 commented Jun 1, 2026

Uh oh!

mdmitry1 commented Jun 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Results after commit 88cdb5f Mon Jun 1 23:19:50 2026 +0300

All inputs are in place

Missing master files

Diffs

SMLP packages

Uh oh!

fbrausse commented Jun 2, 2026

Uh oh!

mdmitry1 left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mdmitry1 commented Jun 2, 2026 •

edited

Loading

Results after commit `88cdb5f` Mon Jun 1 23:19:50 2026 +0300