nseq diverging on trivial example

[CEisenhofer]

Hi copilot,

Check out the c3 branch of this repo and consider running the following SMTLib benchmark:

(set-info :status sat)
(declare-fun a () String)
(declare-fun b () String)

(declare-fun i () Int)
(declare-fun j () Int)

(assert (str.in_re a (re.union (str.to_re "hhhbbb") (str.to_re "bhhh"))))
(assert (= (str.indexof a "hhh" j) i))
(assert (= i 1))
(assert (= j 0))

(check-sat)

The new nseq solver diverges because it runs in an infinite loop, as nielsen_graph::generate_extensions does not know what to do with the str.at atom. This atom [probably introduced by the rewriter, as it is obviously not in the input] should already have been axiomatized. Hence, it should be a Skolem constant, but it is not.

When searching for a fix, make sure that the following benchmark also works:

(set-info :status unsat)
(declare-fun a () String)
(declare-fun b () String)

(declare-fun i () Int)
(declare-fun j () Int)

(assert (str.in_re a (re.union (str.to_re "hhhbbb") (str.to_re "bhhh"))))
(assert (= (str.indexof a "hhh" j) i))

(assert (= i 2))
(assert (> j 0))

(check-sat)