Search results

get_best_solver is costly

Status: Open.

#602 In formalsec/smtml;

· redianthus opened on Apr 13, 2026

bottleneck on Mappings.encode_expr

Status: Open.

#601 In formalsec/smtml;

· redianthus opened on Apr 13, 2026

bottleneck on Expr.simplify

Status: Open.

#600 In formalsec/smtml;

· redianthus opened on Apr 13, 2026

bottleneck on Expr.equal

Status: Open.

#599 In formalsec/smtml;

· redianthus opened on Apr 13, 2026

smtzilla seems to always select Z3

Status: Open.

#598 In formalsec/smtml;

· redianthus opened on Apr 13, 2026

bottleneck in Mappings.clz

Status: Open.

#595 In formalsec/smtml;

· redianthus opened on Apr 12, 2026

use Z.to_bytes when available in a new release

Status: Open.

#594 In formalsec/smtml;

· redianthus opened on Apr 12, 2026

Trivial queries sent to the solvers

Status: Open.

#570 In formalsec/smtml;

· hra687261 opened on Mar 9, 2026

mdx blocks that use z3 are only enabled when the only installed solver is z3

Status: Open.

#565 In formalsec/smtml;

· filipeom opened on Mar 5, 2026

Unimplemented allchar regexp constant in z3 mappings

type: bug

Status: Open.

#561 In formalsec/smtml;

· filipeom opened on Feb 28, 2026

list of unsupported solvers

type: feature

Status: Open.

#555 In formalsec/smtml;

· redianthus opened on Feb 22, 2026

Typed.Bool.symbol, etc. don't check types at all

type: bug

Status: Open.

#552 In formalsec/smtml;

· sim642 opened on Feb 22, 2026