Skip to content

Passthrough HOL unifier when dealing with non-HOL problem - #1032

Merged
mezpusz merged 2 commits into
masterfrom
passthrough-hol-unifier-when-non-hol
Oct 24, 2026
Merged

Passthrough HOL unifier when dealing with non-HOL problem#1032
mezpusz merged 2 commits into
masterfrom
passthrough-hol-unifier-when-non-hol

Conversation

@mezpusz

@mezpusz mezpusz commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Alternative solution to #1030 that fixes #938. I cherry-picked the unit test from #1030.

I'm running an ALASCA regression to see if anything changed. FOL and HOL regressions showed no difference.

@mezpusz

mezpusz commented Oct 21, 2026

Copy link
Copy Markdown
Contributor Author

ALASCA tests over SMTLIB show losing 109 instances probably all unsound previously:


run 0 unsat: 44701 (109) sat: 135 (0) cputime: 46390.70 s instructions: 182019577 Mi memory: 1134924.85 MB
run 1 unsat: 44592 (0) sat: 135 (0) cputime: 46610.98 s instructions: 182351496 Mi memory: 1135954.72 MB

run 0 uniquely proved: 109
SMT-LIB/flat/AUFNIRA::FFT::smtlib.635732.smt2
SMT-LIB/flat/AUFNIRA::FFT::smtlib.635849.smt2
SMT-LIB/flat/AUFNIRA::FFT::smtlib.645715.smt2
SMT-LIB/flat/AUFNIRA::FFT::smtlib.645857.smt2
SMT-LIB/flat/AUFNIRA::FFT::smtlib.653905.smt2
SMT-LIB/flat/AUFNIRA::FFT::smtlib.654080.smt2
SMT-LIB/flat/AUFNIRA::FFT::smtlib.659901.smt2
SMT-LIB/flat/AUFNIRA::FFT::smtlib.662069.smt2
SMT-LIB/flat/AUFNIRA::FFT::smtlib.671895.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.634134.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.636136.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.636226.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.638194.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.638333.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.640330.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.640466.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.647252.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.647389.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.649261.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.655748.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.661907.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.661994.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.663869.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.663953.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.673103.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.673310.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.685476.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.687448.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.697344.smt2
SMT-LIB/flat/AUFNIRA::FFT::z3.697561.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Arrow_Order::smtlib.564898.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1001678.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1002366.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1005475.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1006155.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1009249.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1009905.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1018649.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1019321.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1022406.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.1023044.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.551876.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.572506.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.595005.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.669415.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.669600.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.744184.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.959974.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.960184.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.963443.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.963878.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.964073.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.967139.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.967563.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.967752.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.997847.smt2
SMT-LIB/flat/UFLIA::sledgehammer::FFT::smtlib.998552.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.765745.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.766487.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.768041.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.774341.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.777364.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.780357.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.783350.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.786343.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.801690.smt2
SMT-LIB/flat/UFLIA::sledgehammer::Fundamental_Theorem_Algebra::smtlib.967849.smt2
SMT-LIB/flat/UFLIA::sledgehammer::TwoSquares::smtlib.626558.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1001796.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1002271.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1002488.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1005564.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1006248.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1009314.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1009970.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1018677.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1019353.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1022409.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.1023051.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.593908.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.601420.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.605575.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.742461.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.930847.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.934645.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.960252.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.963484.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.963922.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.964117.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.967167.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.967597.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.967786.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.998474.smt2
SMT-LIB/flat/UFNIA::sledgehammer::FFT::z3.998697.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.769072.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.769814.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.771761.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.777718.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.780741.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.783734.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.786727.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.789720.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.792711.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.795698.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.800351.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.805067.smt2
SMT-LIB/flat/UFNIA::sledgehammer::Fundamental_Theorem_Algebra::z3.807864.smt2
SMT-LIB/flat/UFNIA::sledgehammer::QEpres::z3.974759.smt2
SMT-LIB/flat/UFNIA::sledgehammer::TwoSquares::z3.625214.smt2

MichaelRawson
MichaelRawson approved these changes Oct 21, 2026
View reviewed changes

@MichaelRawson MichaelRawson left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks OK. Is the point that HOL and arithmetic is unsound?

@mezpusz

mezpusz commented Oct 21, 2026

Copy link
Copy Markdown
Contributor Author

The HOL unifier was too eagerly applied even when it was not needed, but otherwise they shouldn't work together yet, that's probably another PhD...

@shalashaska117

shalashaska117 commented Oct 22, 2026

Copy link
Copy Markdown
Contributor

This looks cleaner to me, thanks for carrying over the regression test.

@mezpusz
mezpusz merged commit 7743386 into master Oct 24, 2026
1 check passed
@mezpusz
mezpusz deleted the passthrough-hol-unifier-when-non-hol branch October 24, 2026 06:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@MichaelRawson MichaelRawson MichaelRawson approved these changes
@quickbeam123 quickbeam123 quickbeam123 approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Unsound unsat caused by uwa=alasca_* without -alasca on

4 participants

@mezpusz @shalashaska117 @MichaelRawson @quickbeam123