search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

(get-interpolant) fails with: Overflow encountered when expanding vector #6404

Closed daniel-larraz closed 2 years ago

daniel-larraz commented 2 years ago

The (get-interpolant) command in this SMTLIB script (traffic.txt) returns the following error:

(error "line 921 column 57: Overflow encountered when expanding vector")

z3 version: d4885ab Operating system: Ubuntu 20.04

NikolajBjorner commented 2 years ago

appears fixed. Interpolant happens to be trivial.