7 commits

Author	SHA1	Message	Date
Margus Veanes	195a0486aa	tests(wordeq-ladder): add minimal nseq spurious-unsat reproducer ... Distilled companion to d5-two-var-square.smt2: x.x in (Sigma* "a" Sigma*) with |x|=1 is sat (x="a"), but smt.string_solver=nseq returns unsat. Trigger = regex membership over a str.++ of variable terms + an exact length (str.len = k, or a word equation forcing lengths); default/seq/z3str3 are correct. nseq is a c3-branch-only solver; master is unaffected. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>	2026-07-02 17:32:49 +03:00
Margus Veanes	0b9b6b5869	more unit tests	2026-07-02 14:51:16 +03:00
Nikolaj Bjorner	266008e81f	update seq_model draft ... redo seq_model to be compatible with model_generator	2026-05-03 13:57:56 -07:00
CEisenhofer	14f71ea852	Reuse power variables and symbolic characters	2026-03-31 16:36:10 +02:00
CEisenhofer	63830085b6	Delete unsupported testcases	2026-03-22 13:11:08 +01:00
CEisenhofer	a99b93ef1f	Added testcases	2026-03-20 18:40:55 +01:00
Nikolaj Bjorner	520ee1debc	adding files to test	2026-03-05 13:38:06 -08:00