Package evaluation to test SymbolicSMT on Julia 1.14.0-DEV.1475 (42ad41c179*) started at 2026-01-04T19:00:50.412 ################################################################################ # Set-up # Installing PkgEval dependencies (TestEnv)... Activating project at `~/.julia/environments/v1.14` Set-up completed after 10.26s ################################################################################ # Installation # Installing SymbolicSMT... Resolving package versions... Updating `~/.julia/environments/v1.14/Project.toml` [a0d8a0e1] + SymbolicSMT v1.2.0 Updating `~/.julia/environments/v1.14/Manifest.toml` [47edcb42] + ADTypes v1.21.0 [6e696c72] + AbstractPlutoDingetjes v1.3.2 [1520ce14] + AbstractTrees v0.4.5 [7d9f7c33] + Accessors v0.1.43 [79e6a3ab] + Adapt v4.4.0 [4fba245c] + ArrayInterface v7.22.0 [e2ed5e7c] + Bijections v0.2.2 [fa961155] + CEnum v0.5.0 ⌅ [861a8166] + Combinatorics v1.0.2 [f70d9fcc] + CommonWorldInvalidations v1.0.0 [b152e2b5] + CompositeTypes v0.1.4 [a33af91c] + CompositionsBase v0.1.2 [187b0558] + ConstructionBase v1.6.0 [864edb3b] + DataStructures v0.19.3 [b552c78f] + DiffRules v1.15.1 [ffbed154] + DocStringExtensions v0.9.5 [5b8099bc] + DomainSets v0.7.16 [7c1d4256] + DynamicPolynomials v0.6.4 [4e289a0a] + EnumX v1.0.5 [e2ba6199] + ExprTools v0.1.10 [55351af7] + ExproniconLite v0.10.14 [18e54dd8] + IntegerMathUtils v0.1.3 [8197267c] + IntervalSets v0.7.13 [3587e190] + InverseFunctions v0.1.17 [92d709cd] + IrrationalConstants v0.2.6 [692b3bcd] + JLLWrappers v1.7.1 [ae98c720] + Jieko v0.2.1 [2ab3a3ac] + LogExpFunctions v0.3.29 [1914dd2f] + MacroTools v0.5.16 [2e0e35c7] + Moshi v0.3.7 [102ac46a] + MultivariatePolynomials v0.5.13 [d8a4904e] + MutableArithmetics v1.6.7 [77ba4419] + NaNMath v1.1.3 [bac558e1] + OrderedCollections v1.8.1 [aea7be01] + PrecompileTools v1.3.3 [21216c6a] + Preferences v1.5.1 [27ebfcd6] + Primes v0.5.7 [988b38a3] + ReadOnlyArrays v0.2.0 [3cdcf5f2] + RecipesBase v1.3.4 [189a3867] + Reexport v1.2.2 [ae029012] + Requires v1.3.1 [7e49a35a] + RuntimeGeneratedFunctions v0.5.16 [431bcebd] + SciMLPublic v1.0.1 [efcf1570] + Setfield v1.1.2 [276daf66] + SpecialFunctions v2.6.1 [90137ffa] + StaticArrays v1.9.16 [1e83bf80] + StaticArraysCore v1.4.4 [2efcf032] + SymbolicIndexingInterface v0.3.46 ⌅ [19f23fe9] + SymbolicLimits v0.2.4 [a0d8a0e1] + SymbolicSMT v1.2.0 [d1185830] + SymbolicUtils v4.10.0 [0c5d862f] + Symbolics v7.4.1 [ed4db957] + TaskLocalValues v0.1.3 [8ea1fca8] + TermInterface v2.0.0 [d30d5f5c] + WeakCacheSets v0.1.0 [06b161dc] + Z3 v1.0.4 [efe28fd5] + OpenSpecFun_jll v0.5.6+0 [3eaa8342] + libcxxwrap_julia_jll v0.14.7+0 [1bc4e1ec] + z3_jll v4.15.4+0 [0dad84c5] + ArgTools v1.1.2 [56f22d72] + Artifacts v1.11.0 [2a0f44e3] + Base64 v1.11.0 [ade2ca70] + Dates v1.11.0 [f43a241f] + Downloads v1.7.0 [7b1f6079] + FileWatching v1.11.0 [9fa8497b] + Future v1.11.0 [b77e0a4c] + InteractiveUtils v1.11.0 [ac6e5ff7] + JuliaSyntaxHighlighting v1.13.0 [b27032c2] + LibCURL v1.0.0 [76f85450] + LibGit2 v1.11.0 [8f399da3] + Libdl v1.11.0 [37e2e46d] + LinearAlgebra v1.13.0 [56ddb016] + Logging v1.11.0 [d6f4376e] + Markdown v1.11.0 [ca575930] + NetworkOptions v1.3.0 [44cfe95a] + Pkg v1.14.0 [de0858da] + Printf v1.11.0 [9a3f8284] + Random v1.11.0 [ea8e919c] + SHA v1.0.0 [9e88b42a] + Serialization v1.11.0 [2f01184e] + SparseArrays v1.13.0 [f489334b] + StyledStrings v1.13.0 [fa267f1f] + TOML v1.0.3 [a4e569a6] + Tar v1.10.0 [8dfed614] + Test v1.11.0 [cf7118a7] + UUIDs v1.11.0 [4ec0a83e] + Unicode v1.11.0 [e66e0078] + CompilerSupportLibraries_jll v1.3.0+1 [781609d7] + GMP_jll v6.3.0+2 [deac9b47] + LibCURL_jll v8.17.0+0 [e37daf67] + LibGit2_jll v1.9.2+0 [29816b5a] + LibSSH2_jll v1.11.3+1 [14a3606d] + MozillaCACerts_jll v2025.12.2 [4536629a] + OpenBLAS_jll v0.3.29+0 [05823500] + OpenLibm_jll v0.8.7+0 [458c3c95] + OpenSSL_jll v3.5.4+0 [efcefdf7] + PCRE2_jll v10.47.0+0 [bea87d4a] + SuiteSparse_jll v7.10.1+0 [83775a58] + Zlib_jll v1.3.1+2 [3161d3a3] + Zstd_jll v1.5.7+1 [8e850b90] + libblastrampoline_jll v5.15.0+0 [8e850ede] + nghttp2_jll v1.68.0+1 [3f19e933] + p7zip_jll v17.7.0+0 Info Packages marked with ⌅ have new versions available but compatibility constraints restrict them from upgrading. To see why use `status --outdated -m` Installation completed after 6.51s ################################################################################ # Precompilation # ERROR: LoadError: MethodError: no method matching setindex!(::Base.ScopedValues.ScopedValue{IO}, ::Nothing) The function `setindex!` exists, but no method is defined for this combination of argument types. Stacktrace: [1] top-level scope @ /PkgEval.jl/scripts/precompile.jl:10 [2] include(mod::Module, _path::String) @ Base ./Base.jl:309 [3] exec_options(opts::Base.JLOptions) @ Base ./client.jl:344 [4] _start() @ Base ./client.jl:585 in expression starting at /PkgEval.jl/scripts/precompile.jl:6 caused by: MethodError: no method matching setindex!(::Base.ScopedValues.ScopedValue{IO}, ::Base.DevNull) The function `setindex!` exists, but no method is defined for this combination of argument types. Stacktrace: [1] top-level scope @ /PkgEval.jl/scripts/precompile.jl:7 [2] include(mod::Module, _path::String) @ Base ./Base.jl:309 [3] exec_options(opts::Base.JLOptions) @ Base ./client.jl:344 [4] _start() @ Base ./client.jl:585 Precompilation failed after 16.76s ################################################################################ # Testing # Testing SymbolicSMT Status `/tmp/jl_yitGyl/Project.toml` [1bc83da4] SafeTestsets v0.1.0 [a0d8a0e1] SymbolicSMT v1.2.0 [d1185830] SymbolicUtils v4.10.0 [0c5d862f] Symbolics v7.4.1 [06b161dc] Z3 v1.0.4 [8dfed614] Test v1.11.0 Status `/tmp/jl_yitGyl/Manifest.toml` [47edcb42] ADTypes v1.21.0 [6e696c72] AbstractPlutoDingetjes v1.3.2 [1520ce14] AbstractTrees v0.4.5 [7d9f7c33] Accessors v0.1.43 [79e6a3ab] Adapt v4.4.0 [4fba245c] ArrayInterface v7.22.0 [e2ed5e7c] Bijections v0.2.2 [fa961155] CEnum v0.5.0 ⌅ [861a8166] Combinatorics v1.0.2 [f70d9fcc] CommonWorldInvalidations v1.0.0 [b152e2b5] CompositeTypes v0.1.4 [a33af91c] CompositionsBase v0.1.2 [187b0558] ConstructionBase v1.6.0 [864edb3b] DataStructures v0.19.3 [b552c78f] DiffRules v1.15.1 [ffbed154] DocStringExtensions v0.9.5 [5b8099bc] DomainSets v0.7.16 [7c1d4256] DynamicPolynomials v0.6.4 [4e289a0a] EnumX v1.0.5 [e2ba6199] ExprTools v0.1.10 [55351af7] ExproniconLite v0.10.14 [18e54dd8] IntegerMathUtils v0.1.3 [8197267c] IntervalSets v0.7.13 [3587e190] InverseFunctions v0.1.17 [92d709cd] IrrationalConstants v0.2.6 [692b3bcd] JLLWrappers v1.7.1 [ae98c720] Jieko v0.2.1 [2ab3a3ac] LogExpFunctions v0.3.29 [1914dd2f] MacroTools v0.5.16 [2e0e35c7] Moshi v0.3.7 [102ac46a] MultivariatePolynomials v0.5.13 [d8a4904e] MutableArithmetics v1.6.7 [77ba4419] NaNMath v1.1.3 [bac558e1] OrderedCollections v1.8.1 [aea7be01] PrecompileTools v1.3.3 [21216c6a] Preferences v1.5.1 [27ebfcd6] Primes v0.5.7 [988b38a3] ReadOnlyArrays v0.2.0 [3cdcf5f2] RecipesBase v1.3.4 [189a3867] Reexport v1.2.2 [ae029012] Requires v1.3.1 [7e49a35a] RuntimeGeneratedFunctions v0.5.16 [1bc83da4] SafeTestsets v0.1.0 [431bcebd] SciMLPublic v1.0.1 [efcf1570] Setfield v1.1.2 [276daf66] SpecialFunctions v2.6.1 [90137ffa] StaticArrays v1.9.16 [1e83bf80] StaticArraysCore v1.4.4 [2efcf032] SymbolicIndexingInterface v0.3.46 ⌅ [19f23fe9] SymbolicLimits v0.2.4 [a0d8a0e1] SymbolicSMT v1.2.0 [d1185830] SymbolicUtils v4.10.0 [0c5d862f] Symbolics v7.4.1 [ed4db957] TaskLocalValues v0.1.3 [8ea1fca8] TermInterface v2.0.0 [d30d5f5c] WeakCacheSets v0.1.0 [06b161dc] Z3 v1.0.4 [efe28fd5] OpenSpecFun_jll v0.5.6+0 [3eaa8342] libcxxwrap_julia_jll v0.14.7+0 [1bc4e1ec] z3_jll v4.15.4+0 [0dad84c5] ArgTools v1.1.2 [56f22d72] Artifacts v1.11.0 [2a0f44e3] Base64 v1.11.0 [ade2ca70] Dates v1.11.0 [f43a241f] Downloads v1.7.0 [7b1f6079] FileWatching v1.11.0 [9fa8497b] Future v1.11.0 [b77e0a4c] InteractiveUtils v1.11.0 [ac6e5ff7] JuliaSyntaxHighlighting v1.13.0 [b27032c2] LibCURL v1.0.0 [76f85450] LibGit2 v1.11.0 [8f399da3] Libdl v1.11.0 [37e2e46d] LinearAlgebra v1.13.0 [56ddb016] Logging v1.11.0 [d6f4376e] Markdown v1.11.0 [ca575930] NetworkOptions v1.3.0 [44cfe95a] Pkg v1.14.0 [de0858da] Printf v1.11.0 [9a3f8284] Random v1.11.0 [ea8e919c] SHA v1.0.0 [9e88b42a] Serialization v1.11.0 [2f01184e] SparseArrays v1.13.0 [f489334b] StyledStrings v1.13.0 [fa267f1f] TOML v1.0.3 [a4e569a6] Tar v1.10.0 [8dfed614] Test v1.11.0 [cf7118a7] UUIDs v1.11.0 [4ec0a83e] Unicode v1.11.0 [e66e0078] CompilerSupportLibraries_jll v1.3.0+1 [781609d7] GMP_jll v6.3.0+2 [deac9b47] LibCURL_jll v8.17.0+0 [e37daf67] LibGit2_jll v1.9.2+0 [29816b5a] LibSSH2_jll v1.11.3+1 [14a3606d] MozillaCACerts_jll v2025.12.2 [4536629a] OpenBLAS_jll v0.3.29+0 [05823500] OpenLibm_jll v0.8.7+0 [458c3c95] OpenSSL_jll v3.5.4+0 [efcefdf7] PCRE2_jll v10.47.0+0 [bea87d4a] SuiteSparse_jll v7.10.1+0 [83775a58] Zlib_jll v1.3.1+2 [3161d3a3] Zstd_jll v1.5.7+1 [8e850b90] libblastrampoline_jll v5.15.0+0 [8e850ede] nghttp2_jll v1.68.0+1 [3f19e933] p7zip_jll v17.7.0+0 Info Packages marked with ⌅ have new versions available but compatibility constraints restrict them from upgrading. Testing Running tests... ┌ Warning: The call to compilecache failed to create a usable precompiled cache file for SymbolicSMT [a0d8a0e1-65bc-4be1-9afb-79a704359442] │ exception = Required dependency Base.PkgId(Base.UUID("fa961155-64e5-5f13-b03f-caf6b980ea82"), "CEnum") failed to load from a cache file. └ @ Base loading.jl:2950 ┌ Warning: The call to compilecache failed to create a usable precompiled cache file for Z3 [06b161dc-0161-11ea-0f74-41f836f4024b] │ exception = Required dependency Base.PkgId(Base.UUID("fa961155-64e5-5f13-b03f-caf6b980ea82"), "CEnum") failed to load from a cache file. └ @ Base loading.jl:2950 Basic Functionality Tests: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/basic.jl:6 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/basic.jl:8 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/basic.jl:18 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1103 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/basic.jl:19 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:8 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Basic Satisfiability: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:10 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:11 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:11 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:9 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:9 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:9 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Provability Tests: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:24 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:25 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:25 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:9 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:9 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:9 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Contradictory Constraints: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:36 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:38 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:38 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:9 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:9 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:9 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Complex Expressions: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:45 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:46 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/solver.jl:46 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:9 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:9 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:9 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Single Constraints: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:9 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:11 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:11 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1103 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:12 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:10 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 Multiple Constraints: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:20 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:22 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:22 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:10 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Arithmetic in Constraints: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:29 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:31 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:31 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1103 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:32 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:10 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 Boolean Operations: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:39 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:42 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:42 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:10 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Edge Cases: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:48 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{Any}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:50 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:50 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1103 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/constraints.jl:51 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:10 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:10 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 Comparison Operations: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:9 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:10 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:10 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:11 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Arithmetic Operations: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:20 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:21 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:21 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:11 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Complex Expressions: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:38 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:39 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:39 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:11 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Mixed Variable Types: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:47 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:48 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:49 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:11 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Constants and Literals: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:56 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:7 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:57 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/operations.jl:57 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:11 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:11 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Constraints with Num Types: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:13 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] Constraints(constraints::Vector{Symbolics.Num}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:385 [5] Constraints(constraints::Vector{Symbolics.Num}) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:384 [6] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:7 [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:15 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:15 [inlined] [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1103 [inlined] [12] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [13] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:12 [14] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [15] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [16] eval(m::Module, e::Any) @ Core ./boot.jl:489 [17] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [18] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [19] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [20] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [21] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [22] top-level scope @ none:6 [23] eval(m::Module, e::Any) @ Core ./boot.jl:489 [24] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [25] _start() @ Base ./client.jl:585 issatisfiable with Num: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:25 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] Constraints(constraints::Vector{Symbolics.Num}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:385 [5] Constraints(constraints::Vector{Symbolics.Num}) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:384 [6] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:7 [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:26 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:26 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:12 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 isprovable with Num: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:45 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] Constraints(constraints::Vector{Symbolics.Num}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:385 [5] Constraints(constraints::Vector{Symbolics.Num}) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:384 [6] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:7 [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:46 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:46 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:12 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 resolve with Num: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:60 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] Constraints(constraints::Vector{Symbolics.Num}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:385 [5] Constraints(constraints::Vector{Symbolics.Num}) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:384 [6] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:7 [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:61 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:61 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:12 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 Mixed Num and SymbolicUtils: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:80 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] Constraints(constraints::Vector{Symbolics.Num}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:385 [5] Constraints(constraints::Vector{Symbolics.Num}) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:384 [6] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:7 [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:83 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:87 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:12 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 Integer Variables: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:96 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] Constraints(constraints::Vector{Symbolics.Num}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:385 [5] Constraints(constraints::Vector{Symbolics.Num}) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:384 [6] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:7 [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:98 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:100 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:12 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 Boolean Variables: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:107 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] Constraints(constraints::Vector{Symbolics.Num}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:385 [5] Constraints(constraints::Vector{Symbolics.Num}) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:384 [6] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:7 [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:109 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:111 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:12 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 Complex Symbolics Expressions: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:119 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] Constraints(constraints::Vector{Symbolics.Num}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:385 [5] Constraints(constraints::Vector{Symbolics.Num}) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:384 [6] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:7 [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:120 [inlined] [9] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [10] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/symbolics_frontend.jl:123 [inlined] [11] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [12] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:12 [13] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [14] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [15] eval(m::Module, e::Any) @ Core ./boot.jl:489 [16] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [17] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [18] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:12 [inlined] [19] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [20] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [21] top-level scope @ none:6 [22] eval(m::Module, e::Any) @ Core ./boot.jl:489 [23] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [24] _start() @ Base ./client.jl:585 Issue #14 - Multi-variable arithmetic expressions: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/regression.jl:6 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/regression.jl:6 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/regression.jl:12 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/regression.jl:15 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:13 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:13 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:13 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Power operator support: Error During Test at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/regression.jl:46 Got exception outside of a @test UndefVarError: `libz3` not defined in `Z3.Libz3` Suggestion: check for spelling errors or missing imports. Stacktrace: [1] Z3_mk_config @ ~/.julia/packages/Z3/hj4Zb/src/libz3.jl:540 [inlined] [2] Context @ ~/.julia/packages/Z3/hj4Zb/src/Z3.jl:33 [inlined] [3] Constraints(cs::Vector{SymbolicUtils.BasicSymbolicImpl.var"typeof(BasicSymbolicImpl)"{SymbolicUtils.SymReal}}, solvertype::String) @ SymbolicSMT ~/.julia/packages/SymbolicSMT/Sb3pZ/src/SymbolicSMT.jl:197 [4] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/regression.jl:6 [5] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [6] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/regression.jl:49 [inlined] [7] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [8] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/regression.jl:52 [inlined] [9] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [10] top-level scope @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:13 [11] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [12] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:13 [inlined] [13] eval(m::Module, e::Any) @ Core ./boot.jl:489 [14] top-level scope @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:8 [15] macro expansion @ /opt/julia/share/julia/stdlib/v1.14/Test/src/Test.jl:1995 [inlined] [16] macro expansion @ ~/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:13 [inlined] [17] macro expansion @ ~/.julia/packages/SafeTestsets/raUNr/src/SafeTestsets.jl:28 [inlined] [18] include(mapexpr::Function, mod::Module, _path::String) @ Base ./Base.jl:310 [19] top-level scope @ none:6 [20] eval(m::Module, e::Any) @ Core ./boot.jl:489 [21] exec_options(opts::Base.JLOptions) @ Base ./client.jl:310 [22] _start() @ Base ./client.jl:585 Test Summary: | Pass Error Total Time SymbolicSMT.jl Tests | 8 25 33 31.2s Basic Functionality | 5 1 6 17.2s Basic Functionality Tests | 5 1 6 15.4s SAT Solver Tests | 4 4 2.2s SAT Solver Tests | 4 4 2.1s Basic Satisfiability | 1 1 0.0s Provability Tests | 1 1 0.0s Contradictory Constraints | 1 1 0.1s Complex Expressions | 1 1 2.0s Constraint Construction | 5 5 0.5s Constraint Construction Tests | 5 5 0.4s Single Constraints | 1 1 0.1s Multiple Constraints | 1 1 0.0s Arithmetic in Constraints | 1 1 0.1s Boolean Operations | 1 1 0.0s Edge Cases | 1 1 0.2s Symbolic Operations | 5 5 0.1s Symbolic Operations Tests | 5 5 0.1s Comparison Operations | 1 1 0.0s Arithmetic Operations | 1 1 0.0s Complex Expressions | 1 1 0.0s Mixed Variable Types | 1 1 0.0s Constants and Literals | 1 1 0.0s Symbolics.jl Frontend | 3 8 11 11.0s Symbolics.jl Frontend Tests | 3 8 11 10.1s Constraints with Num Types | 1 1 0.2s issatisfiable with Num | 1 1 0.0s isprovable with Num | 1 1 0.0s resolve with Num | 1 1 0.0s Mixed Num and SymbolicUtils | 1 1 0.0s Integer Variables | 1 1 0.0s Boolean Variables | 1 1 0.0s Complex Symbolics Expressions | 1 1 9.5s Regression Tests | 2 2 0.1s Regression Tests | 2 2 0.0s Issue #14 - Multi-variable arithmetic expressions | 1 1 0.0s Power operator support | 1 1 0.0s RNG of the outermost testset: Random.Xoshiro(0x3b7cf5dc6a3bd5f6, 0xdebe333abab1ca01, 0xc15049b92386c6fd, 0x3a00251b0917a921, 0x344a03e78b98b6d1) ERROR: LoadError: Some tests did not pass: 8 passed, 0 failed, 25 errored, 0 broken. in expression starting at /home/pkgeval/.julia/packages/SymbolicSMT/Sb3pZ/test/runtests.jl:6 Testing failed after 120.39s ERROR: LoadError: Package SymbolicSMT errored during testing Stacktrace: [1] pkgerror(msg::String) @ Pkg.Types /opt/julia/share/julia/stdlib/v1.14/Pkg/src/Types.jl:68 [2] test(ctx::Pkg.Types.Context, pkgs::Vector{PackageSpec}; coverage::Bool, julia_args::Cmd, test_args::Cmd, test_fn::Nothing, force_latest_compatible_version::Bool, allow_earlier_backwards_compatible_versions::Bool, allow_reresolve::Bool) @ Pkg.Operations /opt/julia/share/julia/stdlib/v1.14/Pkg/src/Operations.jl:3067 [3] test @ /opt/julia/share/julia/stdlib/v1.14/Pkg/src/Operations.jl:2916 [inlined] [4] test(ctx::Pkg.Types.Context, pkgs::Vector{PackageSpec}; coverage::Bool, test_fn::Nothing, julia_args::Cmd, test_args::Cmd, force_latest_compatible_version::Bool, allow_earlier_backwards_compatible_versions::Bool, allow_reresolve::Bool, kwargs::@Kwargs{io::IOContext{IO}}) @ Pkg.API /opt/julia/share/julia/stdlib/v1.14/Pkg/src/API.jl:572 [5] kwcall(::@NamedTuple{julia_args::Cmd, io::IOContext{IO}}, ::typeof(Pkg.API.test), ctx::Pkg.Types.Context, pkgs::Vector{PackageSpec}) @ Pkg.API /opt/julia/share/julia/stdlib/v1.14/Pkg/src/API.jl:548 [6] test(pkgs::Vector{PackageSpec}; io::IOContext{IO}, kwargs::@Kwargs{julia_args::Cmd}) @ Pkg.API /opt/julia/share/julia/stdlib/v1.14/Pkg/src/API.jl:172 [7] kwcall(::@NamedTuple{julia_args::Cmd}, ::typeof(Pkg.API.test), pkgs::Vector{PackageSpec}) @ Pkg.API /opt/julia/share/julia/stdlib/v1.14/Pkg/src/API.jl:161 [8] test(pkgs::Vector{String}; kwargs::@Kwargs{julia_args::Cmd}) @ Pkg.API /opt/julia/share/julia/stdlib/v1.14/Pkg/src/API.jl:160 [9] test @ /opt/julia/share/julia/stdlib/v1.14/Pkg/src/API.jl:160 [inlined] [10] kwcall(::@NamedTuple{julia_args::Cmd}, ::typeof(Pkg.API.test), pkg::String) @ Pkg.API /opt/julia/share/julia/stdlib/v1.14/Pkg/src/API.jl:159 [11] top-level scope @ /PkgEval.jl/scripts/evaluate.jl:237 [12] include(mod::Module, _path::String) @ Base ./Base.jl:309 [13] exec_options(opts::Base.JLOptions) @ Base ./client.jl:344 [14] _start() @ Base ./client.jl:585 in expression starting at /PkgEval.jl/scripts/evaluate.jl:228 PkgEval failed after 211.4s: package tests unexpectedly errored