mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-20 01:03:20 +00:00
Code Activity
20347 commits 84 branches 53 tags 204 MiB
Commit graph

80 commits

Author SHA1 Message Date
Copilot
bd0eba812d
Add RCF (Real Closed Field) bindings to C++, Java, C#, and TypeScript (#8171) 
* Initial plan

* Add RCF (Real Closed Field) bindings to C++ API

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

* Add RCF (Real Closed Field) bindings to Java API

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

* Add RCF (Real Closed Field) bindings to C# (.NET) API

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

* Add RCF (Real Closed Field) example for TypeScript/JavaScript API

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

* Add comprehensive RCF implementation summary documentation

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-12 16:34:42 -08:00
Copilot
cfd40d2588
Add set_ast_print_mode() to Python, C#, and TypeScript bindings (#8166) 
* Initial plan

* Add set_ast_print_mode to Python and PrintMode getter to C#

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

* Add setPrintMode to TypeScript Context API

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-11 21:20:32 -08:00
Copilot
5aac5c98b3
Add missing API functions to C++, Java, C#, and TypeScript bindings (#8152) 
* Initial plan

* Add missing API functions to C++, Java, C#, and TypeScript bindings

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

* Fix TypeScript type errors in new API functions

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

* Address code review comments and add documentation

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

* Fix TypeScript async issue in polynomialSubresultants

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

* Delete API_COHERENCE_FIXES.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-01-11 13:59:30 -08:00
Copilot
319db5dbb1
Add missing API methods across language bindings (#8150) 
* Initial plan

* Add API coherence improvements for C#, Python, C++, and TypeScript

- C#: Add SubstituteFuns method to Expr class
- Python: Add update method to ExprRef class
- C++: Add update method to expr class
- TypeScript: Add complete Statistics API with Statistics interface, StatisticsEntry interface, StatisticsImpl class, and statistics() methods for Solver, Optimize, and Fixedpoint

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

* Add Z3_stats import and Statistics types to TypeScript bindings

- Add Z3_stats to imports in types.ts and high-level.ts
- Add Statistics and StatisticsEntry to type imports in high-level.ts
- Fixes missing type references identified in 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-01-11 10:01:04 -08:00
Copilot
2777a39b93
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-01-10 19:44:24 -08:00
Copilot
7c69858b14
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-01-10 14:38:34 -08:00
Copilot
d7579706e2
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-01-10 12:55:08 -08:00
Copilot
6d14d2e3b8
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-01-10 12:04:50 -08:00
Copilot
495e1f44ba
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-01-09 11:26:27 -08:00
Nikolaj Bjorner
3881b6845b
Update high-level.test.ts 2026-01-09 09:34:10 -08:00
Copilot
c324f41eb0
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-01-09 09:03:53 -08:00
Nikolaj Bjorner
926359140b
Remove duplicate unsatCore method in types.ts 
Removed duplicate unsatCore method declaration.
 2026-01-08 20:56:12 -08:00
Copilot
f690afa6b1
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-01-08 19:53:08 -08:00
Copilot
7a35caa60a
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-01-08 18:43:58 -08:00
Copilot
042b6d92b1
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>
 2025-12-15 22:57:46 +00:00
Chris Cowan
ebe8b5dea5
Typescript typedef and doc fixes take 2 (#8078) 
* Fix Typescript typedef to allow `new Context`

* fix init() tsdoc example using nonexistent sat import
 2025-12-15 20:31:20 +00:00
Nikolaj Bjorner
77cb70a082
Revert "Typescript typedef and doc fixes (#8073)" (#8077) 
This reverts commit 6cfbcd19df.
 2025-12-15 17:38:04 +00:00
Chris Cowan
6cfbcd19df
Typescript typedef and doc fixes (#8073) 
* Fix Typescript typedef to allow `new Context`

* fix init() tsdoc example using nonexistent sat import
 2025-12-15 17:03:41 +00:00
Nikolaj Bjorner
ab227c83b2 remove deprecated set_has_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 15:11:59 -08:00
Nikolaj Bjorner
8ba77dfc6b remove deprecated set_has_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 15:10:20 -08:00
Nikolaj Bjorner
682865df24 remove deprecated set_has_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 15:07:27 -08:00
Nikolaj Bjorner
449ce1a012 remove deprecated set_has_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 15:04:40 -08:00
Nikolaj Bjorner
bf6ff56fd6 update package lock 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 16:56:18 -08:00
Nikolaj Bjorner
aad511d40b missing new closure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-06 21:22:23 -07:00
Copilot
7a8ba4b474
Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) 
* Initial plan

* Add datatype type definitions to types.ts (work in progress)

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

* Complete datatype type definitions with working TypeScript compilation

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

* Implement core datatype functionality with TypeScript compilation success

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

* Complete datatype implementation with full Context integration and tests

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>
 2025-08-04 20:58:42 -07:00
Nikolaj Bjorner
6893e782ed add cases for new parameters for ts build 2025-01-22 11:59:36 -08:00
Dmitri
f99e1ee581
Support BitVectors in the TypeScript Optimize API (#7480) 
This is just a change in type declarations to allow calling minimize/maximize with BitVectors.
 2024-12-30 08:49:30 -08:00
Kevin Gibbons
e5f8327483
Update emscripten (#7473) 
* fixes for newer emscripten thread handling behavior

* fix return type for async wrapper functions

* update prettier

* update typescript and fix errors

* update emscripten version in CI

* update js readme about tests
 2024-12-06 18:11:14 -08:00
Yuantian Ding
4be4067f75
Typescript high-level api for Sets (#7471) 2024-12-05 07:00:11 -08:00
Jonas Jongejan
604714ba40
js: Add pseudo-boolean high-level functions (#7426) 
* js: Add pseudo-boolean high-level functions

* Add check for arg length
 2024-11-02 12:34:15 -07:00
Jonas Jongejan
45ef6d0109
js: Adding manual release methods (#7428) 
* js: Adding manual release methods

* Add unregister token

* Add pointer assertion

* Add missing line
 2024-10-22 09:15:49 -07:00
Kevin Gibbons
77aa5280df
wasm: increase timeout in tests (#7401) 2024-09-25 18:33:14 +01:00
Kevin Gibbons
103c5ad71c
wasm: attempt to GC in tests (#7400) 2024-09-25 15:53:36 +01:00
Nikolaj Bjorner
2655301afc comment out simple proofs unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-24 23:01:12 +01:00
Nikolaj Bjorner
716a815ce1 update lock file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-24 11:29:35 +01:00
dependabot[bot]
758d886fac
Bump braces from 3.0.2 to 3.0.3 in /src/api/js (#7261) 
Bumps [braces](https://github.com/micromatch/braces) from 3.0.2 to 3.0.3.
- [Changelog](https://github.com/micromatch/braces/blob/master/CHANGELOG.md)
- [Commits](https://github.com/micromatch/braces/compare/3.0.2...3.0.3)

---
updated-dependencies:
- dependency-name: braces
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-06-19 15:29:38 -07:00
dependabot[bot]
8b04049069
Bump @babel/traverse from 7.19.4 to 7.23.2 in /src/api/js (#6954) 
Bumps [@babel/traverse](https://github.com/babel/babel/tree/HEAD/packages/babel-traverse) from 7.19.4 to 7.23.2.
- [Release notes](https://github.com/babel/babel/releases)
- [Changelog](https://github.com/babel/babel/blob/main/CHANGELOG.md)
- [Commits](https://github.com/babel/babel/commits/v7.23.2/packages/babel-traverse)

---
updated-dependencies:
- dependency-name: "@babel/traverse"
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2023-10-23 15:29:42 -07:00
LufyCZ
19e921290e
increase wasm stack size (#6931) 2023-10-06 11:49:54 +09:00
THE Spellchecker
dc0887db5a
Typo Fixes (#6803) 2023-07-09 11:56:10 -07:00
Guillaume Bagan
0c9a5f69fd
JS/TS: add Optimize class (#6712) 
* implement  Optimize class for the high level Typescript API

* javascript and wasm: add _malloc to exported functions

fix the bug https://github.com/Z3Prover/z3/issues/6709

* javascript: add tests for the Optimize class

* javascript: no reason that minimize and optimize must be constants
 2023-05-06 11:53:43 -07:00
Walden Yan
ede9e5ffc2
[WIP] More TS Binding Features (#6412) 
* feat: basic quantfier support

* feat: added isQuantifier

* feat: expanded functions

* wip: (lambda broken)

* temp fix to LambdaImpl typing issue

* feat: function type inference

* formatting with prettier

* fix: imported from invalid module

* fix isBool bug and dumping to smtlib

* substitution and model.updateValue

* api to add custom func interps to model

* fix: building

* properly handling uint32 -> number conversion in z3 TS wrapper

* added simplify

* remame Add->Sum and Mul->Product

* formatting
 2023-02-11 15:48:29 -08:00
dependabot[bot]
a4f2a1bb2e
Bump json5 from 2.2.1 to 2.2.3 in /src/api/js (#6527) 
Bumps [json5](https://github.com/json5/json5) from 2.2.1 to 2.2.3.
- [Release notes](https://github.com/json5/json5/releases)
- [Changelog](https://github.com/json5/json5/blob/main/CHANGELOG.md)
- [Commits](https://github.com/json5/json5/compare/v2.2.1...v2.2.3)

---
updated-dependencies:
- dependency-name: json5
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
 2023-01-09 09:16:55 +00:00
Nikolaj Bjorner
ea0d09b6c8 add pointer to build parameters to README #6518 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-02 16:49:31 -08:00
Nikolaj Bjorner
4c79e63c1b Update parse-api.ts 2022-10-19 12:52:58 -07:00
Walden Yan
f175fcbb54
JS/TS API Array support (#6393) 
* feat: basic array support

Still need deeper type support for Arrays

* fixed broken format rules

* spaces inside curly

* feat: range sort type inference

* feat: better type inference in model eval

* doc: fixed some incorrect documentation

* feat: domain type inference

* feat: addressed suggestions

* feat: addressed suggestions

* chore: moved ts-expect from deps to dev-deps

* test: added z3guide examples

* fix: removed ts-expect from dependencies again

* docs: fixed some documentation
 2022-10-17 11:10:36 -07:00
Nikolaj Bjorner
f6e4a45f4b Merge branch 'master' of https://github.com/z3prover/z3 2022-08-21 18:28:19 -07:00
Nikolaj Bjorner
daa24ef4ce add missing error check 2022-08-21 18:26:53 -07:00
Bruce Mitchener
6ba9ada1e2
Fix typos. (#6291) 2022-08-21 12:40:07 -07:00
Nikolaj Bjorner
08bf7a6293 fix name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-19 18:22:42 -07:00
Nikolaj Bjorner
665ef2c6ba add missing new 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-19 18:21:03 -07:00