Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Parity in Counterexample-Related Z3 Options for Command-Line vs Language Server #4792

Merged
merged 15 commits into from
Jan 22, 2024
Merged

Parity in Counterexample-Related Z3 Options for Command-Line vs Language Server #4792

Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
1be2388
Counterexample parity for extension vs command line
Nov 16, 2023
d5505f4
Update DafnyRef and dev/news
Nov 16, 2023
8d428bc
Update ProverLogRegression
Nov 16, 2023
77c4e8f
Update existing test
Nov 16, 2023
83cc425
Merge remote-tracking branch 'origin/master' into CounterexampleParity
Jan 19, 2024
d182a13
Enable counterexamples for multiple locations in the program
Jan 19, 2024
65d2c04
Temprorarily add boogie submodule
Jan 19, 2024
00fa2a5
Fix test-generation translation pass and Update tests
Jan 19, 2024
0d7789f
Fix variable printing order and update tests
Jan 19, 2024
8aa183b
Revert "Temprorarily add boogie submodule"
Jan 22, 2024
10002e4
Update Boogie version
Jan 22, 2024
76700d7
Fix customBoogie.patchj
Jan 22, 2024
37bf3aa
Merge branch 'master' into CounterexampleParity
Jan 22, 2024
8515c8e
Update Prover Log test
Jan 22, 2024
c06d769
Update Inverses test
Jan 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update Prover Log test
  • Loading branch information
Aleksandr Fedchin committed Jan 22, 2024
commit 8515c8e7ad35b1679b7b1bc06a05f00ad6641ee5
20 changes: 15 additions & 5 deletions Source/DafnyPipeline.Test/expectedProverLog.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,9 +200,11 @@
(set-option :type_check true)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.delay_units true)
(set-option :model_evaluator.completion true)
(set-option :model.completion true)
(set-option :model.compact false)
(set-option :smt.case_split 3)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
(set-option :smt.arith.solver 2)
Expand Down Expand Up @@ -490,9 +492,11 @@ $generated@@185)))
(set-option :type_check true)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.delay_units true)
(set-option :model_evaluator.completion true)
(set-option :model.completion true)
(set-option :model.compact false)
(set-option :smt.case_split 3)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
(set-option :smt.arith.solver 2)
Expand Down Expand Up @@ -1030,9 +1034,11 @@ $generated@@226))))))
(set-option :type_check true)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.delay_units true)
(set-option :model_evaluator.completion true)
(set-option :model.completion true)
(set-option :model.compact false)
(set-option :smt.case_split 3)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
(set-option :smt.arith.solver 2)
Expand Down Expand Up @@ -1413,9 +1419,11 @@ $generated@@523))))))))
(set-option :type_check true)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.delay_units true)
(set-option :model_evaluator.completion true)
(set-option :model.completion true)
(set-option :model.compact false)
(set-option :smt.case_split 3)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
(set-option :smt.arith.solver 2)
Expand Down Expand Up @@ -1938,9 +1946,11 @@ $generated@@337)))))))))
(set-option :type_check true)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.delay_units true)
(set-option :model_evaluator.completion true)
(set-option :model.completion true)
(set-option :model.compact false)
(set-option :smt.case_split 3)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
(set-option :smt.arith.solver 2)
Expand Down
Loading