mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 15:04:42 +00:00
Code Activity
20377 commits 45 branches 58 tags 178 MiB
Commit graph

17112 commits

Author SHA1 Message Date
Copilot
ce62db18a4 Add Simplifier, Params, and ParamDescrs APIs to TypeScript bindings (#8146) 
* Initial plan

* Add Simplifier, Params, and ParamDescrs APIs to TypeScript bindings

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

* Add Tactic.usingParams and comprehensive documentation for new APIs

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

* Format code with prettier

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

* Add implementation summary documentation

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

* Fix test by using valid parameter for solve-eqs simplifier

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

* Delete IMPLEMENTATION_SUMMARY.md

---------

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-18 20:57:08 -08:00
Copilot
d867eb3cd8 Add Goal, ApplyResult, and Tactic APIs to TypeScript bindings (#8141) 
* Initial plan

* Add Goal, ApplyResult, and enhanced Tactic/Probe APIs to TypeScript bindings

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

* Fix async tactic.apply and add comprehensive tests for new APIs

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

* Address code review feedback: fix proxy handler, factory method, and type improvements

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

* Add API examples documentation and format code with Prettier

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

* Fix merge conflict in test file - complete truncated tactic test

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

* Add test case for tactic.apply method

missing bracket,

* Change tactic from 'simplify' to 'smt'

* Delete src/api/js/TACTICS_API_EXAMPLES.md

---------

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-18 20:57:07 -08:00
Nikolaj Bjorner
767f7eeace fix #8116 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:07 -08:00
Copilot
3a5cf48289 Add Floating-Point and String/Sequence APIs to TypeScript bindings (#8135) 
* Initial plan

* Add FP and String/Seq type definitions to TypeScript bindings

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

* Implement FP and String/Seq in TypeScript high-level bindings

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

* Add comprehensive tests for FP and String/Seq APIs

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

* Fix build errors: Add isFP to test scope and use eqIdentity for Sort comparison

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

* Fix code formatting with Prettier for WASM build

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

* Fix FPNum.value() to use Z3_get_numeral_double instead of parsing string

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

* Simplify length check for empty sequence

Refactor length check for empty sequence in tests.

---------

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-18 20:57:07 -08:00
Copilot
1dc59727c2 Add missing API methods: Java substituteFuns, TypeScript Fixedpoint and substitution APIs (#8138) 
* Initial plan

* Add substituteFuns to Java and substitute methods to TypeScript

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

* Add Fixedpoint (Datalog) API to TypeScript bindings

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

* Improve error message in Java substituteFuns method

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

* Fix TypeScript build error: use .ptr instead of .decl for FuncDecl

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

* Fix TypeScript build errors: handle optional symbols and pointer null checks

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-18 20:57:07 -08:00
Copilot
aff4a61eb3 Add missing array API functions and fix BitVec method typos (#8132) 
* Initial plan

* Add missing API functions: array_default, array_ext, and fix BitVec typos

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

* Add documentation for new array API functions

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

* Fix WebAssembly build: Add default() method to LambdaImpl

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-18 20:57:07 -08:00
Nikolaj Bjorner
617fb60176 Update high-level.test.ts 2026-02-18 20:57:07 -08:00
Copilot
6b3adcf259 Add solver introspection APIs to Java bindings (getUnits, getNonUnits, getTrail) (#8130) 
* Initial plan

* Add getUnits(), getNonUnits(), and getTrail() methods to Java Solver API

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

* Add SolverIntrospectionExample and update Java examples README

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

* Revert changes in examples/java directory, keep only Solver.java API changes

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-18 20:57:07 -08:00
Copilot
5bf49cbd5a Add TypeScript API parity: Solver introspection, congruence closure, and Model sort universe methods (#8129) 
* Initial plan

* Add TypeScript API parity: Solver and Model introspection methods

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

* Format code and add API parity demo example

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

* Add comprehensive API parity documentation

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

* Fix Context usage in tests and demo - use api.Context('main')

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

* Delete src/api/js/API_PARITY.md

* Delete src/api/js/examples/high-level/api-parity-demo.ts

---------

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-18 20:57:07 -08:00
Nikolaj Bjorner
8fddcd7d89 Remove duplicate unsatCore method in types.ts 
Removed duplicate unsatCore method declaration.
 2026-02-18 20:57:06 -08:00
Copilot
c9528cc74e Add AtMost, AtLeast, unsatCore, and reasonUnknown to JS/TS API (#8118) 
* Initial plan

* Add AtMost, AtLeast, checkAssumptions, and unsatCore methods to JS/TS API

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

* Format code with prettier

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

* Add comprehensive documentation for Solver.check, checkAssumptions, and unsatCore methods

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

* Remove redundant checkAssumptions method, use check() for assumptions

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

* Enable unsat_core tracking in test to fix 'unknown' result

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

* Add reasonUnknown() method and use it in test to debug unknown results

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-02-18 20:57:06 -08:00
Copilot
b524f63957 Add missing C# API functions for solver introspection and congruence closure (#8126) 
* Initial plan

* Add missing C# API functions for NonUnits, Trail, and Congruence methods

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

* Fix formatting: remove extra blank lines in new properties

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-18 20:57:06 -08:00
Copilot
3be56ff27b Fix memory lifetime bug in async array parameter handling for JS API (#8125) 
* Initial plan

* Fix async array parameter handling in JS API wrappers

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

* Add test for solver.check() with assumptions

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

* Address code review feedback: add null checks and improve readability

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

* Add unsatCore() method to Solver class

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-18 20:57:05 -08:00
Copilot
d8fe997368 Add missing C++ API methods for congruence closure and model sort universe (#8124) 
* Initial plan

* Add missing C++ API functions for congruence closure and model sort universe

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

* Add error checking and context validation to new API methods

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

* Add documentation for get_sort precondition

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

* Delete examples/c++/test_missing_apis.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-18 20:57:05 -08:00
Nikolaj Bjorner
4ef799ada4 fix #8109 
default behavior is conservative: if the body of a recursive function contains uninterpreted variables they are not rewritten.
Model evaluation will bind values to uninterpreted variables so the filter should not apply here.
 2026-02-18 20:57:05 -08:00
Simon Sobisch
b2db2c8b23 AIX compat (#8113) 
* fix name conflict for struct proc

* aix compat
 2026-02-18 20:57:04 -08:00
bu99ed
cea0f7c427 set source & target version java compile flags in cmake build to match the python/make build for consistent bytecode generation (#8112) 
Co-authored-by: bu99ed <bu99ed@localhost>
 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
b5578ec74e refine maxresw option 2026-02-18 20:57:04 -08:00
Lev Nachmanson
482ece11a8 when deleting the last row from m_e_matrix go over fresh variables defined for this row and mark the rows depending on them as changed 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
a49d2b2067 add a check in entry_invariant() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
51ac976877 update wcnf front-end and add new wcnf strategy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
0da98c1378 catch a conflict with a fractional sum of fixed variables in a term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
cf287e6a64 cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
8b683787d4 fix #8105 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
d0add7e3d8 fix #8045 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
7151c5ac6e fixes to finite domain arrays 
- relevancy could be off and array solver doesn't compensate, #7544
- enforce equalities across store for small domain axioms #8065
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
c495cf42b6 fix #8099 (again) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Lev Nachmanson
5279c7993d assert entry_invariant only when all changes are done 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
d9612d356f fix #8076 
remove unsound "optimization" for correction sets. It misses feasible solutions
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
170febe538 fix #8102 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Ilana Shapiro
6d61efa6b8 Some changes to improve LIA performance (#8101) 
* add user params

* inprocessing flag

* playing around with clause sharing with some arith constraints (complicated version commented out)

* collect shared clauses inside share units after pop to base level (might help NIA)

* dont collect clauses twice

* dont pop to base level when sharing units, manual filter

* clean up code

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
e2df7d3d32 fix #8097 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
7eab06be7e set build be configurable by env 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
5be3c6b4e8 fix indentation 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
d533260445 use new arithmetic solver for AUFLIA, fixes #8090 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:00 -08:00
Nikolaj Bjorner
85c8c6bd6b fix #8092 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:00 -08:00
h-vetinari
a76cc36f13 BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088) 
* Add CMake option to build only Python bindings without rebuilding libz3

Introduce Z3_BUILD_LIBZ3_CORE option (default ON) to control whether libz3 is built.
When set to OFF with Z3_BUILD_PYTHON_BINDINGS=ON, only Python bindings are built
using a pre-installed libz3 library. This is useful for package managers like
conda-forge to avoid rebuilding libz3 for each Python version.

Changes:
- Add Z3_BUILD_LIBZ3_CORE option in src/CMakeLists.txt
- When OFF, find and use pre-installed libz3 as imported target
- Update Python bindings CMakeLists.txt to handle both built and imported libz3
- Add documentation in README-CMake.md with usage examples

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

* Fix CMake export issues when building only Python bindings

Conditionally export Z3_EXPORTED_TARGETS only when Z3_BUILD_LIBZ3_CORE=ON
to avoid errors when building Python bindings without building libz3.

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

* Disable executable and test builds when not building libz3 core

When Z3_BUILD_LIBZ3_CORE=OFF, automatically disable Z3_BUILD_EXECUTABLE
and Z3_BUILD_TEST_EXECUTABLES to avoid build/install errors.

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

* only build src/ folder if Z3_BUILD_LIBZ3_CORE is TRUE

* move z3 python bindings to main CMake

* move more logic to main CMakeLists.txt

* move Z3_API_HEADER_FILES_TO_SCAN to main CMakeLists.txt

---------

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-18 20:57:00 -08:00
Copilot
16596e0b44 Add GitHub Actions workflow to publish JavaScript/TypeScript API documentation (#8084) 
* Initial plan

* Add GitHub Actions workflow to build and publish documentation

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

* Refine documentation workflow to use mk_api_doc.py and install doxygen

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

* Clarify documentation generation step name

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-18 20:56:59 -08:00
Copilot
3c06cee549 Fix DEL character (0x7F) not being escaped in string literals (#8080) 
* Initial plan

* Fix DEL character encoding in string literals

Change condition from `ch >= 128` to `ch >= 127` to include the DEL
character (U+007F, 127) in escaped output. This ensures that the
non-printable DEL control character is properly escaped as \u{7f}
instead of being printed directly.

Also add test cases for DEL and other control characters.

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-18 20:56:59 -08:00
Chris Cowan
d3d770938b Typescript typedef and doc fixes take 2 (#8078) 
* Fix Typescript typedef to allow `new Context`

* fix init() tsdoc example using nonexistent sat import
 2026-02-18 20:56:58 -08:00
Nikolaj Bjorner
e2d568f32b Revert "Typescript typedef and doc fixes (#8073)" (#8077) 
This reverts commit 6cfbcd19df.
 2026-02-18 20:56:58 -08:00
Chris Cowan
13204421e7 Typescript typedef and doc fixes (#8073) 
* Fix Typescript typedef to allow `new Context`

* fix init() tsdoc example using nonexistent sat import
 2026-02-18 20:56:58 -08:00
Ilana Shapiro
34a40c7747 Search tree core resolution optimization (#8066) 
* Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960)

* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet

* adding comments

* fix bug about needing to bubble resolvent upwards to highest ancestor

* fix bug where we need to cover the whole resolvent in the path when bubbling up

* clean up comments

* close entire tree when sibling resolvent is empty

* integrate asms directly into cube tree, remove separate tracking

* try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function

* separate the logic again to avoid mutual recursion

* Refactor search tree closure and resolution logic

Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity.

* apply formatting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Refactor close_with_core to use current node in lambda

* Fix formatting issues in search_tree.h

* fix build issues

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Update smt_parallel.cpp

* Change loop variable type in unsat core processing

* Change method to retrieve unsat core from root

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:58 -08:00
Copilot
1081916973 Implement Z3_optimize_translate for context translation (#8072) 
* Initial plan

* Implement Z3_optimize_translate functionality

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

* Fix compilation errors and add tests for optimize translate

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

* Revert changes to opt_solver.cpp as requested

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-18 20:56:58 -08:00
Nikolaj Bjorner
3a09b0d2b5 remove stale experimental code #8063 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:58 -08:00
Nikolaj Bjorner
3669dc37b3 don't unfold recursive defs if there is an uninterpreted subterm, #7671 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:58 -08:00
Nikolaj Bjorner
b6e8f2b033 disable preprocessing only after formulas are internalized 2026-02-18 20:56:57 -08:00
Nikolaj Bjorner
d59d40a356 allow parsing declared arrays without requiring explicit select 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:57 -08:00
Lev Nachmanson
7a6eb9bb4d fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:57 -08:00
Lev Nachmanson
1200c0bd0c remove unused *_signed_project() methods 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:57 -08:00