Search results

Old version of Z3 causes extremely slow solving times in incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8083 In diffblue/cbmc;

· esteffin opened on Nov 27, 2023

Performance issue with in incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8081 In diffblue/cbmc;

· esteffin opened on Nov 24, 2023

<code>array_exprt</code> is not handled correctly in the incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8080 In diffblue/cbmc;

· esteffin opened on Nov 24, 2023

Broken support for <code>address_of(labelt)</code> in incremental smt2 decision procedure.

Incomplete Incremental SMT2

Status: Open.

#8079 In diffblue/cbmc;

· esteffin opened on Nov 23, 2023

Support for inlined <code>struct</code> type is not yet implemented in incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8078 In diffblue/cbmc;

· esteffin opened on Nov 23, 2023

Support for <code>empty</code> types is not yet implemented in incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8077 In diffblue/cbmc;

· esteffin opened on Nov 23, 2023

<code>byte_extract</code> is not appearing on the rhs of trace assignment when using the incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8076 In diffblue/cbmc;

· esteffin opened on Nov 23, 2023

Support for typecasting between 2 types of arrays is not yet implemented in incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8075 In diffblue/cbmc;

· esteffin opened on Nov 23, 2023

Support for arithmetic Integers is not yet implemented in incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8074 In diffblue/cbmc;

· esteffin opened on Nov 23, 2023

Support for the internal push/pop interface is unimplemented in incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8073 In diffblue/cbmc;

· thomasspriggs opened on Nov 22, 2023

For some tests duplicate and/or missing declarations involving arrays cause problems in incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8072 In diffblue/cbmc;

· thomasspriggs opened on Nov 22, 2023

Large arrays cause out of memory issues during trace generation with incremental smt2 decision procedure

Incomplete Incremental SMT2

Status: Open.

#8071 In diffblue/cbmc;

· thomasspriggs opened on Nov 22, 2023