mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-04 16:26:17 +00:00
Code Activity
20509 commits 43 branches 53 tags 167 MiB
Commit graph

17136 commits

Author SHA1 Message Date
Copilot
50d04d32bf
Add std::initializer_list overloads for BV and arith operations (#8467) 
* Initial plan

* Add std::initializer_list overloads for BV and arith functions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update call sites to use initializer_list format for BV and arith functions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-02 10:00:13 -08:00
Copilot
9007728ddb
Add solve_for and import_model_converter to C++ solver API (#8465) 
* Initial plan

* Add solve_for and import_model_converter methods to C++ API (fixes issues 6 and 8)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback and add comprehensive test

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Remove accidentally committed binary

* Delete examples/c++/test_issues_6_7_8.cpp

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-02 09:01:23 -08:00
Copilot
f5a44cf0b9
Add missing solver APIs to Java and C# bindings (#8464) 
* Initial plan

* Add missing solver APIs for Java and C#

- Issue 3: Add getTrailLevels() to Java and TrailLevels property to C#
- Issue 4: Add cube() iterator to Java (C# already had Cube())
- Issue 5: Add setInitialValue() to Java and SetInitialValue() to C#

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix code review feedback: eliminate redundant trail retrieval

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Improve documentation and efficiency based on code review

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-02 09:01:01 -08:00
Copilot
5fa321368c
Remove redundant explicit default constructors (#8470) 
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
 2026-02-02 08:45:08 +00:00
Copilot
23c531a4c1
Remove redundant default constructors when they're the only constructor (#8461) 
* Initial plan

* Modernize C++ constructors to use C++11 default member initialization - Phase 1

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix theory_pb.h struct definition - move reset() back inside struct

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Modernize C++ constructors to use C++11 default member initialization - Phase 2

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix opt_solver.h - revert rational initialization (complex type)

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Modernize C++ constructors to use C++11 default member initialization - Phase 3

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix sparse_matrix.h - explicitly initialize union member in default constructor

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Remove unnecessary default constructors when they're the only constructor

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-01 16:51:26 -08:00
Copilot
97bf2a5145
Remove redundant non-virtual destructors with = default (#8462) 
* Initial plan

* Remove 6 non-virtual destructors with no code (= default)

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-01 15:22:58 -08:00
Copilot
89e2ceffd0
Use structured bindings for stack entries in theory_datatype (#8442) 
* Initial plan

* Refactor theory_datatype to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix structured binding syntax error in smt_justification.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-31 17:14:47 -08:00
Copilot
e7d46d2566
Refactor expr_stat to use structured bindings for traversal pairs (#8441) 
* Initial plan

* Refactor expr_stat.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix structured binding inside DEBUG_CODE macro in smt_justification.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-31 17:14:02 -08:00
Copilot
ff485eb545
Refactor sat_model_converter to use C++17 structured bindings (#8440) 
* Initial plan

* Refactor sat_model_converter to use C++17 structured bindings

- Updated model_converter::process_stack() to use structured bindings
- Updated model_converter::display() to use structured bindings
- Updated model_converter::expand() to use structured bindings in range-based loop
- All changes compile successfully

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix build error in smt_justification.cpp structured binding

- Changed invalid syntax `enode_pair const & [n1, n2]` to `auto const& [n1, n2]`
- Wrapped for loop in extra parentheses to protect structured binding comma from macro expansion
- Build now completes successfully

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix DEBUG_CODE macro issue with structured bindings

- Reverted DEBUG_CODE block to use .first/.second instead of structured bindings
- Structured bindings with commas cause issues in macros (treated as argument separators)
- Build now works in both debug and release modes

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-31 17:13:07 -08:00
Copilot
db6e15361b
Add Java APIs for polymorphic datatypes (#8438) 
* Initial plan

* Add Java APIs for polymorphic datatypes and type variables

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix code review issue and add documentation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add TypeVarSort.java to CMakeLists.txt for Java bindings

The CMake build was failing because TypeVarSort.java was not included in the Z3_JAVA_JAR_SOURCE_FILES list in src/api/java/CMakeLists.txt. Added it in alphabetical order between TupleSort.java and UninterpretedSort.java.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-31 15:31:36 -08:00
Nuno Lopes
b008b5e926 remove another use of rational::power_of_two() 2026-01-31 14:29:33 +00:00
Nuno Lopes
e1fc837141 minor simplification 2026-01-31 14:19:53 +00:00
Nuno Lopes
09370d7782 optimize has_sign_bit and mod2k to not compute powers of two 
this is very useful for bitvectors of large bitwidths
 2026-01-31 10:38:41 +00:00
Nuno Lopes
10043c37fd fix build 2026-01-30 16:38:23 +00:00
Nuno Lopes
5f835dd99c fix build 2026-01-30 16:29:30 +00:00
Nuno Lopes
095b2bdf59 code simplifications 2026-01-30 15:26:21 +00:00
Nuno Lopes
70a03c7784 constify a constant 
shrinks binary size by 4KB
 2026-01-30 15:01:53 +00:00
Nuno Lopes
7edc4e088a fix build 2026-01-30 14:21:57 +00:00
Copilot
4a1c2f44c5
Fix assertion violation in mpzzp_manager::eq from non-normalized values in peek_fresh (#8439) 
* Initial plan

* Normalize values in peek_fresh and newton_interpolator::add

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Simplify fix - only normalize in peek_fresh with assertions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Delete regressions/issue-8292.smt2

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-29 19:19:59 -08:00
Copilot
0519e6231c
Optimize iterator bit scanning and variable matching per TODO directives (#8416) 
* Initial plan

* Optimize approx_set iterator and variable_intersection populate

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Add clarifying comment for iterator optimization

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-01-29 19:02:13 -08:00
Copilot
477e4d695d
Refactor SMT core: use structured bindings for enode_pair access (#8427) 
* Initial plan

* Refactor SMT core to use C++17 structured bindings for enode pairs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Use const& in structured bindings to avoid copying

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refactor variable unpacking in DEBUG_CODE

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-29 19:01:49 -08:00
Lev Nachmanson
adac953e87 - When removing a fresh var xt, collect all fresh defs that transitively reference it 
- Remove them all from m_fresh_k2xt_terms and m_row2fresh_defs
    - Mark rows containing those vars in m_changed_rows for recalculation
    - Move remove_irrelevant_fresh_defs() before the recalculate loop so all affected rows get recalculated

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-29 06:17:14 -10:00
Copilot
1ec30620ef
Refactor optimization and model to use C++17 structured bindings for pairs (#8426) 
* Initial plan

* Refactor pairs to use C++17 structured bindings in opt and model components

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-28 19:43:57 -08:00
Copilot
0b1d30e86f
[WIP] Refactor NLSAT solver to use structured bindings for variable bounds (#8425) 
* Initial plan

* Refactor NLSAT solver to use structured bindings for variable bounds

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-28 19:42:40 -08:00
Copilot
ebed679287
Refactor dyn_ack.cpp to use structured bindings for app_pair/app_triple (#8359) 
* Initial plan

* Refactor dyn_ack.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Rename structured binding variables from app1/app2/app3 to a1/a2/a3

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-28 19:39:25 -08:00
Copilot
3f9fa59811
Refactor der.cpp topological sort to use structured bindings (#8401) 
* Initial plan

* Refactor der.cpp to use structured bindings for expression/index pairs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix comment to refer to 'e' instead of 't' after structured binding refactor

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-28 19:38:58 -08:00
Nikolaj Bjorner
203afaab07 address #8376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-27 20:22:41 -08:00
Copilot
1d49af5ee6
Refactor sat_solver to use C++17 structured bindings for pair destructuring (#8403) 
* Initial plan

* Refactor sat_solver.cpp to use structured bindings for pairs

- Line 1398: Changed priorities[i].second to use [priority, var]
- Lines 2154-2156: Changed p.first/p.second to use [l1, l2] for binary clauses
- Lines 4182-4184: Eliminated intermediate l1, l2 variables using [l1, l2] binding

This modernizes the code to use C++17 structured bindings instead of .first/.second member accesses.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 20:06:07 -08:00
Copilot
560985893e
Refactor bound_manager to use C++17 structured bindings (#8404) 
* Initial plan

* Refactor bound_manager to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 20:04:01 -08:00
Copilot
7747a17bb7
Refactor theory_array_base to use structured bindings for enode pairs (#8405) 
* Initial plan

* Refactor theory_array_base to use structured bindings for enode pairs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 20:03:18 -08:00
Copilot
ef5ee85bfd
Refactor pb_solver to use structured bindings for wliteral patterns (#8391) 
* Initial plan

* Refactor pb_solver.cpp to use C++17 structured bindings for wliteral patterns

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix active2wlits to avoid unnecessary wliteral reconstruction

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 13:58:14 -08:00
Copilot
8cb403384e
Refactor theory_lra: Use structured bindings for pair patterns (#8387) 
* Initial plan

* Refactor theory_lra.cpp with structured bindings for pair patterns

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 13:57:43 -08:00
Copilot
c4f75bc85a
Refactor seq_rewriter to use C++17 structured bindings (#8381) 
* Initial plan

* Refactor seq_rewriter.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback - move pair declaration inside loop

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 12:06:11 -08:00
Copilot
851e69d7d2
Refactor sat_th to use structured bindings for enode_pair patterns (#8386) 
* Initial plan

* Apply structured bindings to enode_pair patterns in sat_th.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 12:02:28 -08:00
Copilot
e4ba45925e
Refactor theory_seq to use structured bindings for pair patterns (#8390) 
* Initial plan

* Refactor theory_seq.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 12:01:29 -08:00
Copilot
ccc20449dc
Refactor bv_solver to use structured bindings for var_pos patterns (#8384) 
* Initial plan

* Refactor bv_solver.cpp to use C++17 structured bindings for var_pos patterns

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback: simplify bit_trail constructor and remove unnecessary pair reconstruction

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 11:48:21 -08:00
Copilot
ea1ebdeae0
Refactor smt_context to use structured bindings for pair decomposition (#8385) 
* Initial plan

* Refactor smt_context.cpp to use C++17 structured bindings for pair patterns

- Replace .first/.second access with structured bindings in reset_tmp_clauses()
- Replace .first/.second access with structured bindings in decide_clause()
- Replace .first/.second access with structured bindings in init_assumptions()
- Eliminate 3 intermediate variable assignments
- 4 refactoring sites across 3 functions
- Verified successful compilation and all tests pass

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 11:47:31 -08:00
Copilot
ffa8ef4cee
Refactor pb_rewriter to use structured bindings for expression/coefficient pairs (#8380) 
* Initial plan

* Refactor pb_rewriter to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 11:46:28 -08:00
Copilot
01948e168b
Add polymorphic datatype support to ML API (#8378) 
* Initial plan

* Add ML bindings for polymorphic datatypes (mk_type_variable and mk_polymorphic_sort)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add polymorphic datatype example for ML API

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Delete examples/ml/polymorphic_datatype_example.ml

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-27 11:44:35 -08:00
Copilot
cd774b6fdb
Refactor sat_anf_simplifier to use C++17 structured bindings (#8358) 
* Initial plan

* Refactor sat_anf_simplifier.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 09:59:26 -08:00
Nikolaj Bjorner
76d46ee48a Revert "Refactor find_tactic_cmd to use std::optional<tactic_cmd*> (#8331)" 
This reverts commit 7b182c9440.
 2026-01-26 13:20:03 -08:00
Nikolaj Bjorner
3f26d42215 Revert "Refactor find_probe() to use std::optional (#8334)" 
This reverts commit 49817bc259.
 2026-01-26 13:19:56 -08:00
Nikolaj Bjorner
7a2eea6f40 Revert "Refactor find_psort_decl() to return std::optional<psort_decl*> (#8339)" 
This reverts commit 445f995c54.
 2026-01-26 13:19:51 -08:00
Copilot
0a68837ef2
Expose timestamp method in sls_context (#8347) 
* Initial plan

* Expose timestamp method in sls_context

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-26 11:27:27 -08:00
Nikolaj Bjorner
4a29326eaa
Reset timestamp for variables in sat_ddfw.cpp 2026-01-26 10:12:05 -08:00
Nikolaj Bjorner
d18cc5629a
Update timestamp on variable flip in ddfw 2026-01-26 10:11:14 -08:00
Nikolaj Bjorner
a4e123b900
Update sat_ddfw.h 2026-01-26 10:10:04 -08:00
Nikolaj Bjorner
8a0207700c
Fix implicit conversion warnings: use UINT_MAX instead of -1 for unsi… (#8342) 
* Fix implicit conversion warnings: use UINT_MAX instead of -1 for unsigned variables

Replace implicit conversion from negative literal to unsigned type
with explicit UINT_MAX constant to eliminate compiler warnings.

Fixed 10 instances across 6 files:
- src/ast/rewriter/bv_rewriter.cpp: 1 instance
- src/ast/sls/sls_bv_tracker.h: 2 instances
- src/math/lp/dioph_eq.cpp: 3 instances
- src/math/lp/lp_primal_core_solver.h: 2 instances
- src/muz/transforms/dl_mk_array_instantiation.cpp: 1 instance
- src/muz/transforms/dl_mk_synchronize.cpp: 1 instance

These changes preserve the exact same runtime behavior (UINT_MAX
equals the wrapped value of -1 for unsigned types) while making
the code more explicit and warning-free.

* Update bv_rewriter.cpp

---------

Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
 2026-01-25 22:35:43 -08:00
Nikolaj Bjorner
023377f3c8 fix underflow bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-25 21:10:11 -08:00
Nikolaj Bjorner
e65aa0e7d5 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-25 19:50:52 -08:00